r:(
). 
x,y:. (x r y) 
(x E y)
h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n)))Prop. x E yx,y:. Dec(x E y) h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n)))R:(TTProp).
(x,y:T. Dec(x R y)) 
(r:(TT). x,y:T. (x r y) (x R y))
[3]| 1 | 4. r:(). x,y:. (x r y) (x E y) h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n))) |
About:
 |  |  |  |  |  |  |