fact: Definition filter (f : K -> V -> bool) (m : map) : map := fold (fun k_v acc => let '(k,v) := k_v in if f k v then add k v acc else acc) empty m.
imports: RelationClasses ExtLib.Structures.Monad ExtLib.Structures.Reducible