proposition: Lemma tape_local_l_move_left' rs (x : sig) ls : tape_local_l (tape_move_left' rs x ls) = rs.
proof: Proof. destruct rs; cbn; reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM