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