fact: Fixpoint lookup (l : list (A * B)) : B := match l with | nil => default | (el', v)::l' => if @eqA_dec el el' then v else lookup l' end.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)