proposition: Lemma fold_Add m1 m2 k e i : ~In k m1 -> Add k e m1 m2 -> eqA (fold f m2 i) (f k e (fold f m1 i)).
proof: Proof. Proof using st Hf Hf'. intros Hm1 Hm2. rewrite 2 fold_spec_right. set (f':=uncurry f). change (f k e (fold_right f' i (rev (bindings m1)))) with (f' (k,e) (fold_right f' i (rev (bindings m1)))). assert (NoDupA eqk (rev (bindings m1))) by (auto with * ). assert (NoDupA eqk (rev (bindings m2))) by (auto with * ). apply fold_right_add_restr with (R:=complement eqk)(eqA:=eqke); auto with *. - intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. now apply Hf. - unfold complement, eq_key_elt, eq_key, Duo, Fst. repeat red; intuition eauto with map. - intros (k1,e1) (k2,e2) z1 z2; unfold eq_key, f', uncurry, Fst; simpl. eapply Hf'; now eauto. - rewrite <- NoDupA_altdef; auto. - rewrite InA_rev, <- bindings_mapsto_iff by (auto with * ). firstorder. - intros (a,b). rewrite InA_cons, 2 InA_rev, <- 2 bindings_mapsto_iff, 2 find_mapsto_iff by (auto with * ). unfold eq_key_elt,Duo; simpl. rewrite Hm2, !find_spec, add_mapsto_new; intuition (auto with map). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)