proposition: Lemma bVforall_ok : forall n (v : vector A n), bVforall v = true <-> Vforall v.
proof: Proof. induction v; simpl. tauto. rewrite andb_eq, f_ok. tauto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)