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