proposition: Lemma ToSingleTape_Terminates : projT1 ToSingleTape ↓ ToSingleTape_T.
proof: Proof. exact (@Loop_Terminates (start (projT1 pM))). Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)