proposition: Lemma vector_S : forall (A : Set)(n : nat)(v : Vector.t A (S n)), exists a : _, exists v' : _, v = Vector.cons _ a _ v'.
proof: Proof. intuition. induction n, v using Vector.rectS. econstructor. econstructor. eauto. econstructor. econstructor. eauto. Qed.
imports: Bvector Arith