proposition: Lemma mirror_tapes_involution (t : tapes sig n) : mirror_tapes (mirror_tapes t) = t.
proof: Proof. unfold mirror_tapes. apply Vector.eq_nth_iff. intros ? ? ->. erewrite !Vector.nth_map; eauto. apply mirror_tape_involution. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM