proposition: Lemma fold_identity : forall m : t elt, Equal (fold (@add _) m (empty _)) m.
proof: Proof. intros. apply fold_rec with (P:=fun m acc => Equal 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: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface