proposition: Lemma fold_Add_Above m1 m2 x e {A}(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A)(Hf:Proper (K.eq==>eq==>eqA==>eqA) f) : Above x m1 -> Add x e m1 m2 -> eqA (fold f m2 i) (f x e (fold f m1 i)).
proof: Proof. intros. rewrite 2 fold_spec_right. set (f':=uncurry f). transitivity (fold_right f' i (rev (bindings m1 ++ (x,e)::nil))). apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *. - apply Hf; auto. - apply eqlistA_rev. apply bindings_Add_Above; auto. - rewrite distr_rev; simpl. reflexivity. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)