proposition: Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A), Proper (E.eq==>eq==>eqA==>eqA) f -> Equal m1 m2 -> eqA (fold f m1 i) (fold f m2 i).
proof: Proof. intros m1 m2 A eqA st f i Hf Heq. rewrite 2 fold_spec_right. apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. - intros (k,e) (k',e') (Hk,He) a a' Ha; simpl in *; apply Hf; auto. - apply eqlistA_rev. apply elements_Equal_eqlistA. auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface