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