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