proposition: Lemma mirror_tape_inv_rightof' t ls x : rightof ls x = mirror_tape t -> t = leftof ls x.
proof: Proof. intros. destruct t; cbn in *; congruence. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM