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