2. U: Type
3. P: T
UProp4.
x:T, y:U. Dec(P(x,y))5. p: T
U
Dec(p/l,r. P(l,r))
T,U:Type, P:(TUProp). (x:T, y:U. Dec(P(x,y))) 
(p:(TU). Dec(p/l,r. P(l,r)))
| 1 | 1. T: Type 2. U: Type 3. P: T UProp4. x:T, y:U. Dec(P(x,y))5. p: T U Dec(p/l,r. P(l,r)) |
About:
 |  |  |  |  |  |  |  |