proposition: Lemma map_b : forall m x (f:elt->elt'), mem x (map f m) = mem x m.
proof: Proof. intros; do 2 rewrite mem_find_b; rewrite map_o. destruct (find x m); simpl; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface