proposition: Lemma HaltL_enumeration : { e : nat -> option term | enumerator e HaltL }.
proof: Proof. apply (semi_decider_enumerator enumerator__T_term (proj2_sig HaltL_semi_decision)). Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts) Undecidability.L.L Undecidability.L.Enumerators.term_enum Undecidability.L.Computability.Seval