proposition: Lemma Vapp_cons : forall a n1 n2 (v1 : vector A n1) (v2 : vector A n2), Vapp (Vcons a v1) v2 = Vcons a (Vapp v1 v2).
proof: Proof. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)