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