proposition: Lemma fold_add m k e i : ~In k m -> eqA (fold f (add k e m) i) (f k e (fold f m i)).
proof: Proof. Proof using st Hf Hf'. intros. now apply fold_Add. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)