proposition: Lemma fold_Proper {A}(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A) : Proper (K.eq==>eq==>eqA==>eqA) f -> Proper (Equal==>eqA==>eqA) (fold f).
proof: Proof. intros Hf m1 m2 Heq i i' Hi. f_equiv; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)