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