proposition: Lemma L_recognisable_HaltL {X} {Hreg : encodable X} (p : X -> Prop) : L_recognisable p -> p ⪯ HaltL.
proof: Proof. intros. eapply L_recognisable'_recognisable in H as (f & H_f). exists (fun x0 => f (enc x0)). intros x. rewrite H_f. unfold converges, HaltL. setoid_rewrite eval_iff. firstorder. subst. eapply eproc_equiv in 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