proposition: Lemma mirror_tape_inv_midtape t r1 r2 x : mirror_tape t = midtape r1 x r2 -> t = midtape r2 x r1.
proof: Proof. intros. destruct t; cbn in *; congruence. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM