proposition: Lemma L_recognisable'_recognisable {X} `{encodable X} (p : X -> Prop) : L_recognisable p -> L_recognisable' p.
proof: Proof. intros (f & [c_f] & H_f). exists (lam (mu (lam (ext f 1 0)))). intros. assert (((lam (mu (lam ((ext f 1) 0)))) (enc x)) >* mu (lam (ext f (enc x) 0))) by now Lsimpl. rewrite H0. rewrite mu_spec. - rewrite H_f. split; intros [n]; exists n. Lsimpl. now rewrite H1. eapply enc_extinj. now assert ((lam (((ext f) (enc x)) 0)) (ext n) == enc (f x n)) as <- by now Lsimpl. - Lproc. - intros. exists (f x n). now Lsimpl. 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