proposition: Lemma projection X Y {HX : encodable X} {HY : encodable Y} (p : X * Y -> Prop) : L_enumerable p -> L_enumerable (fun x => exists y, p (x,y)).
proof: Proof. intros (f & [cf] & ?). exists (fun n => match f n with Some (x, y) => Some x | None => None end). split. - econstructor. extract. - intros; split. + intros [y ?]. eapply H in H0 as [n]. exists n. now rewrite H0. + intros [n ?]. destruct (f n) as [ [] | ] eqn:E; inv H0. exists y. eapply H. eauto. 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