proposition: Lemma destruct_vector_single {X : Type} (v : Vector.t X 1) : v = [| Vector.hd v |].
proof: Proof. rewrite (Vector.eta v). generalize (Vector.tl v). now apply Vector.case0. Qed.
imports: Undecidability.Shared.Libs.PSL.EqDec Coq.Vectors(Fin Vector)