proposition: Lemma destruct_tape {X : Type} (ts : tapes X 1) : ts = [| Vector.hd ts |].
proof: Proof. unfold tapes in *. rewrite (Vector.eta ts). generalize (Vector.tl ts). now apply Vector.case0. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM