proposition: Lemma Exists_exists l : Exists P l ↔ ∃ x, x ∈ l ∧ P x.
proof: Proof. split. - induction 1 as [x|y ?? [x [??]]]; exists x; by repeat constructor. - intros [x [Hin ?]]. induction l; [by destruct (not_elem_of_nil x)|]. inv Hin; subst; [left|right]; auto. Qed.
imports: stdpp(options)