proposition: Lemma mirror_tape_move_right' rs (x : sig) ls : mirror_tape (tape_move_right' rs x ls) = tape_move_left' ls x rs.
proof: Proof. now destruct ls; cbn. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM