proposition: Lemma VSn_eq : forall n (v : vector A (S n)), v = Vcons (Vhead v) (Vtail v).
proof: Proof. intros. change (Vcons (Vhead v) (Vtail v)) with (Vid v). apply Vid_eq. Defined.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)