proposition: Lemma mapi_mapsto_iff {elt elt'} m x b (f:key->elt->elt') : Proper (K.eq==>Logic.eq==>Logic.eq) f -> (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m).
proof: Proof. rewrite <-find_spec. setoid_rewrite <-find_spec. intros Pr. rewrite mapi_find' by trivial. destruct (find x m); simpl; split. - injection 1 as <-. now exists e. - intros (a,(->,H)). now injection H as <-. - discriminate. - intros (a,(_,H)). discriminate. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)