fact: Definition update (x:key)(f : option elt -> option elt) m := match f (find x m) with | Some e => add x e m | None => remove x m end.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)