fact: Fixpoint lookup `{EqDec a} {b} (dflt : b) (v : list (a * b)) (x : a) : b := match v with | nil => dflt | cons (k, v) xs => if eq_dec k x then v else lookup dflt xs x end.
imports: Coq.Lists.List Equations(Equations) Equations.Type.EqDec Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Applicative Category.Theory.Coq.Monad Category.Theory.Coq.Maybe Coq.Lists.List