proposition: Corollary Sdom : forall A x (m : S.t A), Dom.In x (S.fold (fun x _ acc => Dom.add x acc) m Dom.empty) <-> S.In x m.
proof: Proof. intros. rewrite Sdom_aux. fsetdec. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface