proposition: Lemma mapi_1bis {elt elt'} m x e (f:key->elt->elt') : Proper (K.eq==>Logic.eq==>Logic.eq) f -> MapsTo x e m -> MapsTo x (f x e) (mapi f m).
proof: Proof. intros. destruct (mapi_1 f H0) as (y,(->,H2)). trivial. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)