proposition: Lemma fold_identity m : fold (@add _) m empty == m.
proof: Proof. intros. apply fold_rec with (P:=fun m acc => acc == m); auto with map. intros m' Heq k'. rewrite empty_o. case_eq (find k' m'); auto; intros e'; rewrite <- find_mapsto_iff. intro; elim (Heq k' e'); auto. intros k e a m' m'' _ _ Hadd Heq k'. red in Heq. rewrite Hadd, 2 add_o, Heq; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)