proposition: Lemma MTM_to_stM : HaltMTM ⪯ HaltTM 1.
proof: Proof. unshelve eexists. { intros [[n sig] M ts]. exact (existT2 _ _ (sig' sig) (M' M) (ts' ts)). } intros [[n sig] M ts]. apply MTM_to_stM_correct. Qed.
imports: Undecidability.TM(Single.StepTM TM) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes) Undecidability.Synthetic.Definitions