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