proposition: Lemma bVexists_ok : forall n (v : vector A n), bVexists v = true <-> Vexists v.
proof: Proof. intros. rewrite bVexists_ok_Vin. tauto. intros. rewrite f_ok. tauto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)