我有一个目标，其中有一个存在变量 ?x。为了证明这一点，我需要破坏一个术语 t，并且在破坏 t 产生的不同情况下，实例化 ?x 的术语应该不同，这样才是正确的。
当我完成第一种情况的证明后，Coq 根据第一种情况实例化 ?x，这使得第二种情况无法证明。有没有办法将形式的目标变成P(?x)？exists x,P(x)或者还有其他方法可以解决我遇到的问题？
AskOverflow.Dev
存在性变量只是您不知道如何或不想写的术语的快捷方式。特别是，它只有一个实例，因为它代表一个尚未明确书写的固定术语。特别是，在
exists x, P x逻辑上并不意味着P ?x。对于您的情况，我认为解决方案是永远不要引入?x，即避免引入它的策略（通常是eapply）。