proposition: Lemma exists_spec : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> (exists_ f s = true <-> Exists (fun x => f x = true) s).
proof: Proof. unfold Exists; induction s; simpl; intros. - firstorder. + discriminate. + inv. - destruct (f a) eqn:F. + firstorder. + rewrite IHs; auto. firstorder. inv. * setoid_replace a with x in F; auto; congruence. * exists x; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists