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