Перезапись термина внутри выражения с независимой типизацией завершается неудачно по неизвестной причине

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

Как указано в справочном руководстве :

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 требуетСетоид, чтобы проверить, является ли iff равенством множества.