proposition: Lemma remove_fold_1: forall i s x, In x s -> eqA (f x (fold f (remove x s) i)) (fold f s i).
proof: Proof. intros. symmetry. apply fold_2 with (eqA:=eqA); auto with set relations. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide