proposition: Lemma nb_occ_app : forall (B : Type) a (l1 l2 : list (A * B)), nb_occ a (l1++l2) = nb_occ a l1 + nb_occ a l2.
proof: Proof. fix nb_occ_app 3. intros B a l1; case l1; clear l1; simpl. intros l2; reflexivity. intros p l1 l2; case p; clear p; intros a1 _; simpl. case (eq_bool a a1). simpl; rewrite nb_occ_app; reflexivity. rewrite nb_occ_app; reflexivity. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)