x:T. 
y:(T
). z:T. y(z) 
(x R z)f:(TT). x,z:T. f(x,z) (x R z) r:(TT). x,y:T. (x r y) (x R y)TPropx,y:T. Dec(x R y) r:(TT). x,y:T. (x r y) (x R y)Q:(ABProp). (x:A. y:B. Q(x,y)) 
(f:(AB). x:A. Q(x,f(x)))
[T;T;
x,y. z:T. y(z) (x R z)]| 1 | x:T. y:(T). z:T. y(z) (x R z) |
| 2 | 4. f:(TT). x,z:T. f(x,z) (x R z) r:(TT). x,y:T. (x r y) (x R y) |
About:
 |  |  |  |  |  |  |  |