proposition: Lemma mapi_find' {elt elt'} (f:key->elt->elt') : Proper (K.eq==>Logic.eq==>Logic.eq) f -> forall m x, find x (mapi f m) = option_map (f x) (find x m).
proof: Proof. intros. destruct (mapi_find f m x) as (y,(Hy,->)). destruct (find x m); simpl; trivial. now rewrite Hy. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)