x:T. 
y:
. f(x) 
yf@0:(T
). x:T. f(x) f@0(x) g:(T). t:T. f(t) g(t)Propt:T. Dec(f(t)) g:(T). t:T. f(t) g(t)Q:(ABProp). (x:A. y:B. Q(x,y)) 
(f:(AB). x:A. Q(x,f(x)))
[T;;
t,b. f(t) b]| 1 | x:T. y:. f(x) y |
| 2 | 4. f@0:(T). x:T. f(x) f@0(x) g:(T). t:T. f(t) g(t) |
About:
 |  |  |  |  |  |  |  |