proposition: Lemma HaltL_undec : undecidable (HaltL).
proof: Proof. apply (undecidability_from_reducibility HaltMTM_undec). eapply HaltMTM_to_HaltL. Qed.
imports: Undecidability.L.L Undecidability.Synthetic.Undecidability Undecidability.Synthetic(DecidabilityFacts EnumerabilityFacts) Undecidability.L.Enumerators.term_enum Undecidability.TM.TM Undecidability.TM.TM_undec Undecidability.L.Reductions.TM_to_L