fact: Fixpoint findWithDefault `{EqDec k} (d : v) (i : k) (m : Map) : v := match m with | Empty => d | Add i' x m => if eq_dec i i' then x else findWithDefault d i m end.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib