2. R: T
TProp3.
x,y:T. Dec(x R y)
r:(TT
). x,y:T. (x r y) 
(x R y) T:Type, R:(TTProp). (x,y:T. Dec(x R y)) 
(r:(TT). x,y:T. (x r y) (x R y))| 1 | 1. T: Type 2. R: T TProp3. x,y:T. Dec(x R y) r:(TT). x,y:T. (x r y) (x R y) |
About:
 |  |  |  |  |  |  |  |