proposition: Lemma mapi_o m x (f:key->elt->elt') : Proper (K.eq==>Logic.eq==>Logic.eq) f -> find x (mapi f m) = option_map (f x) (find x m).
proof: Proof. intros; now apply mapi_find'. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)