proposition: Lemma HaltL_semi_decision : { f : term -> nat -> bool | semi_decider f HaltL }.
proof: Proof. exists (fun t n => match eva n t with Some _ => true | None => false end). intros s. split. + intros [t [n Hn]%eval_iff%eval_seval]. exists n. now rewrite (seval_eva Hn). + intros [n Hn]. destruct (eva n s) as [t|] eqn:E. * exists t. now apply eval_iff, (@seval_eval n), eva_seval. * easy. Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts) Undecidability.L.L Undecidability.L.Enumerators.term_enum Undecidability.L.Computability.Seval