proposition: Lemma bVforall2_aux_ok : forall n1 (v1 : vector A n1) n2 (v2 : vector B n2), bVforall2_aux v1 v2 = true <-> Vforall2_aux v1 v2.
proof: Proof. induction v1; simpl; intros. destruct v2. intuition. intuition. destruct v2. intuition. rewrite andb_eq, f_ok, IHv1. tauto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)