proposition: Lemma L_enumerable_enum {X} `{encodable X} (p : X -> Prop) : L_enum p -> L_enumerable p.
proof: Proof. intros (f & [cf] & Hf). exists (F1 f). split. - econstructor. extract. - destruct Hf as [CX HX]. intros x. unfold F1. now rewrite list_enumerator_to_enumerator. Qed.
imports: Undecidability.L(Computability.MuRec) Undecidability.L.Datatypes(LNat LOptions LProd) Undecidability.Synthetic(DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.L.Datatypes.List(List_basics List_nat) Datatypes