proposition: Lemma midtape_tape_local_l_cons_right t r1 r2 x : tape_local_l t = x :: r1 /\ right t = r2 <-> t = midtape r1 x r2.
proof: Proof. rewrite midtape_tape_local_l_cons. intuition subst; cbn; auto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM