proposition: Lemma add_fold : forall i s x, In x s -> eqA (fold f (add x s) i) (fold f s i).
proof: Proof. intros; apply fold_equal; auto with set. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide