fact: Fixpoint Vforall n (v : vector A n) { struct v } : Prop := match v with | Vnil => True | Vcons a w => P a /\ Vforall w end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)