proposition: Lemma Vforall2_dec n (v : vector A n) (w : vector B n) : {Vforall2 v w}+{~Vforall2 v w}.
proof: Proof. unfold Vforall2. apply Vforall2_aux_dec. Defined.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)