proposition: Lemma bVforall2_ok : forall n (v1 : vector A n) (v2 : vector B n), bVforall2 v1 v2 = true <-> Vforall2 v1 v2.
proof: Proof. intros n v1 v2. intuition. unfold Vforall2. apply bVforall2_aux_ok. unfold bVforall2 in H. hyp. unfold bVforall2. apply bVforall2_aux_ok. unfold Vforall2 in H. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)