proposition: Lemma mapi_find {elt elt'}(f:key->elt->elt') m x : exists y, K.eq y x /\ find x (mapi f m) = option_map (f y) (find x m).
proof: Proof. destruct (find x m) eqn:E; simpl. - rewrite find_spec, <- bindings_spec1 in *. rewrite InA_alt in *. destruct E as ((y,e') & (E1,E2) & IN). simpl in *. subst e'. exists y. split; [easy| ]. rewrite find_spec, <- bindings_spec1, InA_alt. exists (y,f y e). split; [easy| ]. rewrite mapi_spec, in_map_iff. now exists (y,e). - exists x. split; [easy| ]. rewrite <- not_in_find in *. rewrite <- not_in_find in E. contradict E. destruct E as (e,M). rewrite <- bindings_spec1, mapi_spec, InA_alt in M. destruct M as ((y,e') & (E1,E2) & IN). simpl in *; subst e'. rewrite in_map_iff in IN. destruct IN as ((z,e0) & [= <- _] & IN). exists e0. rewrite <- bindings_spec1, InA_alt. firstorder. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)