proposition: Lemma Vforall2_aux_dec : forall n1 (v1 : vector A n1) n2 (v2 : vector B n2), {Vforall2_aux v1 v2} + {~Vforall2_aux v1 v2}.
proof: Proof. induction v1; destruct v2; simpl; auto. destruct (IHv1 n0 v2); intuition. destruct (R_dec h h0); intuition. Defined.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)