proposition: Lemma mirror_tape_injective (t1 t2 : tape sig) : mirror_tape t1 = mirror_tape t2 -> t1 = t2.
proof: Proof. destruct t1, t2; intros H; cbn in *; congruence. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM