proposition: Lemma exists_1 : forall s f, @compat_bool elt E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
proof: Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface