proposition: Lemma mirror_tapes_nth (tapes : tapes sig n) (k : Fin.t n) : (mirror_tapes tapes)[@k] = mirror_tape (tapes[@k]).
proof: Proof. intros. eapply VectorSpec.nth_map; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM