proposition: Lemma mapi_1 {elt elt'}(m: t elt)(x:key)(e:elt)(f:key->elt->elt') : MapsTo x e m -> exists y, K.eq y x /\ MapsTo x (f y e) (mapi f m).
proof: Proof. destruct (mapi_find f m x) as (y,(Hy,Eq)). intro H. exists y; split; trivial. rewrite <-find_spec in *. now rewrite Eq, H. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)