proposition: Lemma map_find {elt elt'}(f:elt->elt') m x : find x (map f m) = option_map f (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,f e). split; [easy| ]. rewrite map_spec, in_map_iff. now exists (y,e). - rewrite <- not_in_find in *. rewrite <- not_in_find in E. contradict E. destruct E as (e,M). rewrite <- bindings_spec1, map_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)