proposition: Lemma Exists_eq_exists_mem : forall P l, Exists P l = (exists x, mem x l /\ P x).
proof: Proof. Proof using. Hint Constructors mem. introv. extens. induction l as [|y l']. { iff M (x&M&H). { inverts M. } { inverts M. } } { iff M (x&M&H). { inverts M as N. { exists* y. } { forwards (x&M&H): (proj1 IHl') N. exists* x. } } { destruct (mem_cons_inv M) as [N|N]. { subst*. } { applys* Exists_tail. } } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)