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