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