proposition: Lemma map_induction : forall P : t elt -> Type, (forall m, Empty m -> P m) -> (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') -> forall m, P m.
proof: Proof. intros. apply (@fold_rec _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface