proposition: Lemma atStart_contains (t : tape sigSim) (tps : list (tape sig)) (T : tapes sig n) : length tps = n -> atStart t tps -> vector_to_list T = tps -> t ≃ T.
proof: Proof. clear pM F. intros HL HStart HToList. unfold contains_tapes, atStart in *. subst. f_equal. f_equal. f_equal. unfold encode_tapes. f_equal. auto. 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)