proposition: Lemma fold_diff_inter : forall i s s', eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i).
proof: Proof. intros. transitivity (fold f (union (diff s s') (inter s s')) (fold f (inter (diff s s') (inter s s')) i)). 1:symmetry; apply fold_union_inter; auto. transitivity (fold f s (fold f (inter (diff s s') (inter s s')) i)). - apply fold_equal; auto with set. - apply fold_init; auto. apply fold_1; auto with set. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide