proposition: Lemma tape_midtape_current_left t ls s : current t = Some s -> left t = ls -> t = midtape ls s (right t).
proof: Proof. destruct t; cbn; congruence. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM