展开后出现“fix”是什么原因？

Question

在展开我所能做的一切，试图摆脱归纳假设中我不想要的符号后，我留下了：

X: Type
test: X -> bool
x: X
l: list X
IHl: (fix existsb
         (X : Type) (test : X -> bool) 
         (l : list X) {struct l} : bool :=
         fold orb (map test l) false) X test l =
      negb
        ((fix forallb
            (X : Type) (test : X -> bool)
            (l : list X) {struct l} : bool :=
            fold andb (map test l) true) X
           (fun x : X => negb (test x)) l)

最终嵌入的两个固定点应该尽可能地进行评估，因为我已经>介绍'他们的参数；如果只是用它们的参数来评估它们，我的 IHl 将是完美的。

我不清楚为什么在这种情况下这些不会进行评估。由于这个例子来自逻辑基础，我没有提供更多的解决方案，希望这足以询问我可以将什么策略应用于 IHl 以使 coq 实际上使用我的参数进行重写我正在寻找。

Answer 1

我想我不太明白，但看来我的情况基本上与这个问题相似：

为什么不能在 Coq 中使用抽象值计算固定定义的表达式？

似乎解决方法是在中destruct l为了确保所有情况都以构造函数开始，然后消除两个冗余情况中的固定点，使证明或多或少直接从那里开始。

如果有一篇文章能更好地启发我，让我了解为什么这里无法获得一级替代，那就太好了，因为我看不出有任何理由不采用适用于这种情况的策略。