fact: Definition combine (f : K -> V -> V -> V) (m1 m2 : map) : map := fold (fun k_v acc => let '(k,v) := k_v in match lookup k acc with | None => add k v acc | Some v' => add k (f k v v') acc end) m2 m1.
imports: RelationClasses ExtLib.Structures.Monad ExtLib.Structures.Reducible