fact: Fixpoint Vmap n (v : vector A n) : vector B n := match v with | Vnil => Vnil | Vcons a v' => Vcons (f a) (Vmap v') end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)