proposition: Lemma nTM_to_MTM n : HaltTM n ⪯ HaltMTM.
proof: Proof. unshelve eexists. - intros [Sig M t]. exists (n, Sig); eassumption. - intros [Sig M t]. easy. Qed.
imports: Undecidability.TM(Single.StepTM TM) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes) Undecidability.Synthetic.Definitions