coq - 不能统一两个相同的假设

Question

我在上下文中有两个假设，但是当我尝试apply一个到另一个时，我得到了错误unable to unify。我应该能够统一它们。这两个假设如下

IHl : forallb func l = true -> All (fun x : X => func x = true) l H1 : All (fun x : X => func x = true) l

我的目标是通过将 IHl 应用于 H1 从 IHl 中获得前提。

Answer 1

这是初学者普遍的困惑。当用于假设时，该apply策略的工作原理如下：如果H1 : A -> B和H2 : A，则apply H1 in H2替换H2为H2 : B。因此，为了使您的证明成功，您必须IHl : All ... l -> forallb func l = true在上下文中具有相反的含义或假设H1 : forallb func l = true。