2. Z: Type
3. P: T
ZProp4.
x:T, y:Z. Dec(P(x,y))
f_p:(TZ
). x:T, y:Z. P(x,y) 
f_p(x,y)
T,Z:Type, P:(TZProp). (x:T, y:Z. Dec(P(x,y))) 
(f_p:(TZ). x:T, y:Z. P(x,y) f_p(x,y))
| 1 | 1. T: Type 2. Z: Type 3. P: T ZProp4. x:T, y:Z. Dec(P(x,y)) f_p:(TZ). x:T, y:Z. P(x,y) f_p(x,y) |
About:
 |  |  |  |  |  |  |  |  |  |