5. R: T
Prop6. (
f:(
nT). Bij(n; T; f)) & (
t:T. Dec(R(t)))
Dec(t:T. R(t))
T:Type, R:(TProp). (f:((n-1)T). Bij((n-1); T; f)) & (t:T. Dec(R(t))) 
Dec(t:T. R(t)) T:Type, R:(TProp). (f:(nT). Bij(n; T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t))| 1 | 4. T: Type 5. R: T Prop6. ( f:(nT). Bij(n; T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t)) |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |