根据Arthur的建议，我将我的Fixpoint关系更改为相互的Inductive关系，该关系"建立"游戏之间的不同比较，而不是"向下钻取"。
但现在我收到了一个全新的错误信息：
Error: Parameters should be syntactically the same for each inductive type.
我认为错误信息的意思是，所有这些相互感应的定义都需要完全相同的参数。
我知道有一些简单的方法可以绕过这个问题（未使用的虚拟变量、长的函数类型，其中所有内容都在“forall”内部），但我不明白为什么我必须这样做。
有人能解释一下相互感应类型限制背后的逻辑吗？有更优雅的写法吗？这种限制是否意味着彼此之间的归纳调用都必须使用相同的参数（在这种情况下，我不知道任何绕过这个问题的方法，除了可怕的大量代码复制）？
（所有类型和术语的定义，例如compare_quest、game、g1side等，在first question中都没有改变。）
Inductive gameCompare (c : compare_quest) : game -> game -> Prop :=
| igc : forall g1 g2 : game,
innerGCompare (nextCompare c) (compareCombiner c) (g1side c) (g2side c) g1 g2 ->
gameCompare c g1 g2
with innerGCompare (next_c : compare_quest) (cbn : combiner) (g1s g2s : side)
: game -> game -> Prop :=
| compBoth : forall g1 g2 : game,
cbn (listGameCompare next_c cbn (g1s g1) g2)
(gameListCompare next_c cbn g1 (g2s g2)) ->
innerGCompare next_c cbn g1s g2s g1 g2
with listGameCompare (c : compare_quest) (cbn : combiner) : gamelist -> game -> Prop :=
| emptylgCompare : cbn_init cbn -> forall g2 : game, listGameCompare c cbn emptylist g2
| otlgCompare : forall (g1_cdr : gamelist) (g1_car g2 : game),
(cbn (listGameCompare c cbn g1_cdr g2) (gameCompare c g1_car g2)) ->
listGameCompare c cbn (listCons g1_car g1_cdr) g2
with gameListCompare (c : compare_quest) (cbn : combiner) : game -> gamelist -> Prop :=
| emptyglCompare : cbn_init cbn -> forall g1 : game, gameListCompare c cbn g1 emptylist
| otglCompare : forall (g1 g2_car : game) (g2_cdr : gamelist),
(cbn (gameListCompare c cbn g1 g2_cdr) (gameCompare c g1 g2_car)) ->
gameListCompare c cbn g1 (listCons g2_car g2_cdr).
在CGT中，通常有两个玩家（称为
Left和Right）轮流进行游戏，最后一个移动的玩家获胜。每个游戏（意味着每个游戏中的每个位置）可以被看作是Left选项的集合和Right选项的集合，写成{G_L | G_R}。比较两个游戏时，它们可以以四种不同的方式进行比较：<、>、=或||。如果
B对于Left来说比A严格更好，无论谁先走，那么游戏A < B。如果A对于Left来说比B更好，则A > B。如果两个游戏等价（在这样的意义上，即游戏A + -B的总和是零游戏，因此先手的玩家输），则A = B。如果哪个游戏对于Left更好取决于谁先走，则A || B。
比较两个游戏的一种方法如下：
如果
A的所有Left子节点都小于或等于B，并且A是B的所有右子节点的父节点，则A <= B。如果
A有一个右子节点小于或等于B，或者A小于或等于B的任何左子节点，则A <| B。同样地，对于
>=和>|也是如此。
因此，通过观察这些关系中哪一对适用于游戏 A 和 B，可以确定是 A < B (A<=B 且 A<|B)、A=B (A<=B 且 A>=B)、A > B (A>=B 且 A>|B)，还是 A || B (A<|B 且 A>|B)。
这里是 CGT维基百科文章。