fact: Fixpoint filter `(f : v → bool) `(m : Map k v) : Map k v := match m with | Empty => Empty | Add i x m => if f x then Add i x (filter f m) else filter f m end.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib