编辑：我找到了！我忘记了强制。请忽略这个:)
我正在学习 ssreflect 并坚持如何在这里进行。我的证明状态如下：
n, n0 : nat
============================
n = n0 -> n == n0
起初，我尝试了 move/eqP，因为我认为这会将 eqP “应用”到 n=n0，其中“应用”的意思是“从 eqP 给出的反射中获取 n==n0”。然而，这种尝试产生了：
Illegal application (Non-functional construction):
The expression "eqP ?i" of type "?x = ?y"
cannot be applied to the term
"?y0" : "?T0"
我对 y0 和 T0 应该是什么感到困惑。我也试过
intros H. eapply (introT eqP) in H.
产生了错误
Unable to apply lemma of type "?x = ?y -> ?x == ?y"
on hypothesis of type "n = n0".
我试图将显式参数 n0 和 n 传递给 eqP，只是为了看看它是否可以工作，
pose proof (eqP n n0).
但这给出了一个错误
In environment
n, n0 : nat
H : n = n0
The term "n" has type "nat"
while it is expected to have type
"is_true (?x == ?y)".
因此，似乎 eqP 既想要又不想要 ?x 和 ?y 的显式实例化。我真的很感激一些概念上的解释，为什么 move/eqP 的行为不像我认为的那样，以及 eqP 和 (introT eqP) 的类型实际上发生了什么。
如果相关，我正在导入
From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool eqtype.
来自 ssreflect。
谢谢你。