proposition: Lemma map_o m x (f:elt->elt') : find x (map f m) = option_map f (find x m).
proof: Proof. apply map_find. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)