proposition: Lemma exists_2 : forall (s : t) (f : elt -> bool), compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
proof: Proof. intros s f; unfold exists_; case M.exists_; intuition; inversion H0. Qed.
imports: FSetInterface