proposition: Lemma tape_left_move_right (t : tape sig) (x : sig) : current t = Some x -> left (tape_move_right t) = x :: left t.
proof: Proof. intros H. destruct t; cbn in *; try congruence. inv H. destruct l0; cbn; reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM