proposition: Lemma removelast_length (X : Type) (xs : list X) : length (removelast xs) = length xs - 1.
proof: Proof. induction xs as [ | x xs IH]. - cbn. reflexivity. - cbn. destruct xs as [ | x' xs]; cbn in *. + reflexivity. + f_equal. rewrite IH. lia. 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)