proposition: Lemma L_enumerable_recognisable : L_recognisable' p.
proof: Proof. Proof using c_f c_d H_f H_d. exists [L_HOAS λ x, !!mu (λ y, !!(ext test) x y)]. intros. split; intros. - eapply H_f in H0 as [n H0]. edestruct (mu_complete (proc_test x)) with (n := n). + intros. exists (test x n0). cbn. now Lsimpl. + cbn. Lsimpl. unfold test. rewrite H0. destruct (H_d x x); intuition. + exists (ext x0). split; try Lproc. cbn. Lsimpl. now rewrite H1. - destruct H0 as (v & ? & ?). edestruct (mu_sound (proc_test x)) with (v := v) as (n & ? & ? & _). + intros. exists (test x n). cbn. now Lsimpl. + Lproc. + rewrite <- H0. symmetry. cbn. now Lsimpl. + subst. eapply H_f. exists n. assert ([L_HOAS (λ y, !! (ext test) !! (enc x) y) !!(ext n)] == ext (test x n)). cbn. now Lsimpl. cbn in *. rewrite H2 in *. eapply unique_normal_forms in H3;[|Lproc..]. eapply inj_enc in H3. unfold test in H3. destruct (f n); inv H3. destruct (H_d x x0); firstorder congruence. 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