proposition: Lemma map_in_iff : forall m x (f : elt -> elt'), In x (map f m) <-> In x m.
proof: Proof. split; intros; eauto with map. destruct H as (a,H). exists (f a); auto with map. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface