依赖类型表达式内的术语重写由于未知原因失败

Question

这是一个更大的证明的简化片段，它捕获了有问题的行为。

Section foo.
  Parameter t : Type.
  Parameter x : t.
  Parameter y : t.
  Parameter prop : x = y <-> True.
  Parameter prop2 : x = y.
  Lemma lemma : forall e : t, x = y.
    rewrite prop2.
    intro e; trivial.
    Qed.
End foo.

当你用rewrite prop代替rewrite prop2时，coq失败并出现隐式错误。然而，在我看来，coq应该在重写步骤后产生forall e : t, True。有人能帮我一下吗?

Answer 1

如参考手册所述:

rewrite term
This tactic applies to any goal. The type of term must have the form
forall (x1:A1) … (xn:An)eq term1 term2.
where eq is the Leibniz equality or a registered setoid equality.

但prop不具有莱布尼茨等式:

Coq < Unset Printing Notations.
Coq < Print prop.
prop : iff (eq x y) True

所以coq要求Setoid检查iff是否为Setoid相等