proposition: Lemma map_b m x (f:elt->elt') : mem x (map f m) = mem x m.
proof: Proof. rewrite !mem_find_b, map_o. now destruct (find x m). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)