2. R: T
Prop3. (
f:(
0T). Bij(0; T; f)) & (
t:T. Dec(R(t)))
Dec(t:T. R(t)) T:Type, R:(TProp). (f:(0T). Bij(0; T; f)) & (t:T. Dec(R(t))) 
Dec(t:T. R(t))| 1 | 1. T: Type 2. R: T Prop3. ( f:(0T). Bij(0; T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t)) |
About:
 |  |  |  |  |
 |  |  |  |