proposition: Lemma map_1 {elt elt'}(m: t elt)(x:key)(e:elt)(f:elt->elt') : MapsTo x e m -> MapsTo x (f e) (map f m).
proof: Proof. rewrite <- !find_spec, map_find. now intros ->. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)