proposition: Lemma Vexists_eq : forall n (v : vector A n), Vexists v <-> exists x, Vin x v /\ P x.
proof: Proof. induction v; simpl; intuition. destruct H. intuition. exists h. intuition. destruct H1. exists x. intuition. destruct H1. intuition. subst. auto. right. apply H0. exists x. intuition. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)