proposition: Lemma L_enumerable_ext X `{encodable X} p q : L_enumerable p -> (forall x : X, p x <-> q x) -> L_enumerable q.
proof: Proof. intros (f & cf & Hf) He. exists f; split; eauto. intros ?. rewrite <- He. eapply Hf. 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