proposition: Lemma midtape_tape_local_l_cons t r1 x : tape_local_l t = x :: r1 <-> t = midtape r1 x (right t).
proof: Proof. split. - intros H1. destruct t; cbn in *; congruence. - intros H1. destruct t; cbn in *; inv H1. auto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM