proposition: Lemma HaltL_enumerator_spec : enumerator HaltL_enumerator HaltL.
proof: Proof. exact (proj2_sig HaltL_enumeration). Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts) Undecidability.L.L Undecidability.L.Enumerators.term_enum Undecidability.L.Computability.Seval