fact: Fixpoint Vapp n1 n2 (v1 : vector A n1) (v2 : vector A n2) : vector A (n1+n2) := match v1 with | Vnil => v2 | Vcons a v' => Vcons a (Vapp v' v2) end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)