proposition: Lemma mirror_tapes_injective (t1 t2 : tapes sig n) : mirror_tapes t1 = mirror_tapes t2 -> t1 = t2.
proof: Proof. intros H. unfold mirror_tapes in *. apply Vector.eq_nth_iff. intros ? ? ->. eapply Vector.eq_nth_iff with (p1 := p2) in H; eauto. erewrite !Vector.nth_map in H; eauto. now apply mirror_tape_injective. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM