proposition: Lemma mapi_2 {elt elt'}(m: t elt)(x:key)(f:key->elt->elt') : In x (mapi f m) -> In x m.
proof: Proof. destruct (mapi_find f m x) as (y,(Hy,Eq)). rewrite !in_find. intro H; contradict H. now rewrite Eq, H. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)