proposition: Lemma removelast_cons (X : Type) (xs : list X) (x : X) : xs <> nil -> removelast (x :: xs) = x :: removelast xs.
proof: Proof. destruct xs as [ | x' xs']; cbn. - congruence. - intros _. 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)