proposition: Lemma mirror_tape_move_left (t : tape sig) : mirror_tape (tape_move_left t) = tape_move_right (mirror_tape t).
proof: Proof. destruct t; cbn; auto. destruct l; cbn; auto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM