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

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 prop2通过rewrite prop COQ失败，神秘的错误。然而在我的看法coq应该在重写步骤后产生forall e : t, True。谁能帮我这个？

Answer 1

正如reference manual说：

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是setiod平等。