proposition: Lemma midtape_tape_local_cons t r2 x : tape_local t = x :: r2 <-> t = midtape (left t) x r2.
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