我想使用与库中的count_occ函数相关的引理(count_occ_In(。我已经在Coq脚本中导入了库。但我仍然无法使用它。如果我复制count_occ&来自scipt库的eq_dec，然后它就可以工作了。我的问题是，当我包含库模块时，为什么要重新定义函数。请指导我如何只添加库模块来编写引理(不再定义函数(？。
有了额外的信息，这应该对你有用：
Require Import List Arith.
Import ListNotations.
Check count_occ.
Search nat ({?x = ?y} + {?x <> ?y}).
Definition count_occ_nat := count_occ Nat.eq_dec.
Definition count_occ_In_nat := count_occ_In Nat.eq_dec.
Check count_occ_nat.
Check count_occ_In_nat.
看看我是如何使用Check来查找count_occ采用的参数的，以及我是如何用Search来查找等式函数可判定性的合适实例的。
count_occ是这样写的，因为它应该适用于具有可判定等式的任何类型的列表，但要使用它，你需要一个证明，证明你的类型等式是可判定的，你必须明确地给出这个证明。
在现代定义中，可以使此类参数隐式，并使用类型类自动填充可判定等式等信息，但count_occ对此有一个显式参数，因此必须提供它