proposition: Lemma fold_equal : forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
proof: Proof. intros. rewrite 2 fold_spec_right. apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. apply eqlistA_rev. apply sort_equivlistA_eqlistA; auto with set. red; intro a; do 2 rewrite <- elements_iff; auto. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide