fact: Fixpoint maybeLookup `{EqDec a} {b} (v : list (a * b)) (x : a) : Maybe b := match v with | (k, v) :: xs => if eq_dec k x then Just v else maybeLookup xs x | _ => Nothing 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