Require Import Undecidability.L.L Undecidability.TM.TM.
Require Import Undecidability.L.Reductions.TM_to_L.
Require Import Undecidability.TM.TM_undec.
Require Import Undecidability.Synthetic.Undecidability.
Lemma HaltL_undec :
undecidable HaltL.
Proof.
apply (undecidability_from_reducibility HaltMTM_undec).
eapply HaltMTM_to_HaltL.
Qed.
Require Import Undecidability.L.Reductions.TM_to_L.
Require Import Undecidability.TM.TM_undec.
Require Import Undecidability.Synthetic.Undecidability.
Lemma HaltL_undec :
undecidable HaltL.
Proof.
apply (undecidability_from_reducibility HaltMTM_undec).
eapply HaltMTM_to_HaltL.
Qed.