proposition: Lemma fold_equal : forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
proof: Proof. intros i s; pattern s; apply set_induction; clear s; intros. - transitivity i. + apply fold_1; auto. + symmetry; apply fold_1; auto. rewrite <- H0; auto. - transitivity (f x (fold f s i)). + apply fold_2 with (eqA := eqA); auto. + symmetry; apply fold_2 with (eqA := eqA); auto. unfold Add in *; intros. rewrite <- H2; auto. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide