proposition: Lemma foldkeys_Add m1 m2 k e i : ~In k m1 -> Add k e m1 m2 -> eqA (foldkeys m2 i) (f k (foldkeys m1 i)).
proof: Proof. Proof using st Hf Hf'. intros Hm1 Hm2. unfold foldkeys. set (g := fun _ _ => _) in Hf'. change (f k) with (g k e). apply fold_Add; auto. clear - Hf. intros k k' Hk _ _ _ a a' Ha. now apply Hf. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)