proposition: Lemma MTM_to_stM_correct : HaltsTM M ts <-> HaltsTM M' ts'.
proof: Proof. unfold HaltsTM. split. - intros [? [? [? ?]%TM_sTM_simulation']]. do 2 eexists. eassumption. - now intros ?%TM_sTM_simulation'. Qed.
imports: Undecidability.TM(Single.StepTM TM) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes) Undecidability.Synthetic.Definitions