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