fact: Fixpoint nb_occ (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) (a : A) (l : list (A * B)) {struct l} : nat := match l with | nil => 0 | (a',_) :: tl => if (eqA a a') then S (nb_occ eqA a tl) else nb_occ eqA a tl end.
imports: List Arith