Closed ghost closed 10 years ago
theory bug extends root context let 'P:ℙ' let 'Q:ℙ' show (normalize '(x ↦ y ↦ ⊤) P Q')
displays:
(((x : ℙ ↦ y : ℙ ↦ ⊤) P) Q) = ((y : ℙ ↦ ⊤) Q)
The same problem occurs with equating terms, such as when comparing a declared theorem with the final theorem in its proof.
displays:
The same problem occurs with equating terms, such as when comparing a declared theorem with the final theorem in its proof.