fact: Fixpoint Vforall2_aux n1 n2 (v1 : vector A n1) (v2 : vector B n2) : Prop := match v1, v2 with | Vnil, Vnil => True | Vcons a v, Vcons b w => R a b /\ Vforall2_aux v w | _, _ => False end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)