proposition: Lemma fold_union: forall i s s', (forall x, ~(In x s/\In x s')) -> eqA (fold f (union s s') i) (fold f s (fold f s' i)).
proof: Proof. intros. transitivity (fold f (union s s') (fold f (inter s s') i)). { apply fold_init; auto. symmetry; apply fold_1; auto with set. unfold Empty; intro a; generalize (H a); set_iff; tauto. } apply fold_union_inter; auto. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide