proposition: Lemma tape_move_right_left (t : tape) (s : sig) : current t = Some s -> tape_move_left (tape_move_right t) = t.
proof: Proof. intros H1. destruct t; cbn in *; inv H1; auto; destruct l; auto; destruct l0; auto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM