proposition: Lemma exists_spec : forall s f, @compat_bool elt E.eq f -> (exists_ f s = true <-> Exists (fun x => f x = true) s).
proof: Proof. intros. apply xexists_spec. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface