proposition: Lemma exists_spec : forall f, Proper (E.eq==>Logic.eq) f -> (exists_ f s = true <-> Exists (fun x => f x = true) s).
proof: Proof. intros; symmetry; apply MF.exists_iff; auto. Qed.
imports: FSetInterface FSetFacts MSetInterface MSetFacts