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