fact: Fixpoint find (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) (a : A) (l : list (A * B)) {struct l} : option (B) := match l with | nil => None | (a1,b1) :: l => if eqA a a1 then Some b1 else find eqA a l end.
imports: List Arith