proposition: Lemma fold_add : forall m k e i, ~In k m -> eqA (fold f (add k e m) i) (f k e (fold f m i)).
proof: Proof. intros. apply fold_Add; try red; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface