proposition: Lemma tape_right_move_right (t : tape sig) : right (tape_move_right t) = tl (right t).
proof: Proof. destruct t; cbn; auto. apply tape_right_move_right'. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM