proposition: Lemma Vadd_cons : forall x n (v : vector A (S n)), Vadd v x = Vcons (Vhead v) (Vadd (Vtail v) x).
proof: Proof. intro x. destruct n; intro v; rewrite (VSn_eq v) at 1; refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)