我已经找到了一个证据(Coq版本8.13.1，使用infotheo(，其中上下文假设是目标，只需要一个"%B"；附件。我知道它表示"是真的"，但如何进行证明？
(展开is_true不能摆脱"%B"，重写H和应用H不起作用(。
A: finType
B: eqType
i: B
i0: A
X: A -> B
H: (X i0 == i)%B
===
(1/1)
X i0 = i
如有任何建议，不胜感激。
%B表示这是在不同的范围中解析的。等号在H和目标中意味着不同的东西。它是==vs=btw.
您可以关闭注释来查看这两个术语的真正含义。
==可能比=弱。
感谢您的回答。解决了这个问题
move/eqP in H.
apply H.
Qed.