proposition: Lemma bVexists_ok_Vin : forall n (v : vector A n), (forall x, Vin x v -> (f x = true <-> P x)) -> (bVexists v = true <-> Vexists v).
proof: Proof. induction v; simpl. intuition. split; intros. rewrite orb_eq in H0. destruct H0. rewrite H in H0. auto. auto. rewrite IHv in H0. auto. intros. rewrite H. tauto. auto. destruct H0. rewrite <- H in H0. rewrite H0. refl. auto. rewrite <- IHv in H0. rewrite H0. bool. refl. intros. rewrite H. tauto. auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)