问题的证明可以在这里找到。在当前状态下，我想在假设eqveq中展开eqvid和eqvneg，以简化投影，得到两个不同函数之间的矛盾等式。然而，这两个术语是使用assert策略作为子目标合成的，并且当前环境似乎对术语的值没有记忆。我知道我可以手工写出这两项，但在我看来这很麻烦。是否有一种更优雅的方法来恢复在解决子目标时生成的定义?
Incant:
unshelve epose (eqvid := _ : isequiv bool bool).
pose/set是透明的，而assert不是。_变成了一个新的存在变量(或者更标准的说法是统一变量)。正常的pose会失败，因为它无法求解变量，但epose会跳过检查。存在变量通常不会被战术直接攻击(它们是通过统一解决的)，所以它们会被自动搁置，但unshelve会将其控制的战术所产生的所有变量转化为目标。
将断言替换为以下内容(如果需要，您可以自定义标记)和
apply (f_equal (fun f => f false)) in eqveq.
discriminate.
完成你的证明。
注意，如果您这样做，证明状态将很快变得不可读。避免这种情况的一个技巧是使用
Definition hidden {A} {x : A} : A := x.
使用和
unshelve epose (eqvid := hidden : isequiv bool bool).
。然后假设不会显示混乱的项，直到你揭示它。