proposition: Lemma app_comm_cons' (A : Type) (x y : list A) (a : A) : x ++ a :: y = (x ++ [a]) ++ y.
proof: Proof. now rewrite <- app_assoc. 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)