n ~ T
m:. m ~ {t:T| B(t) } Fin({t:T| B(t) })
Propf:(nT). Bij(n; T; f)
t:T. Dec(B(t)) Fin({t:T| B(t) })n:, T:Type, B:(TProp).
(n ~ T) & (t:T. Dec(B(t))) 
(m:. m ~ {t:T| B(t) })
[n;T;B]| 1 | n ~ T |
| 2 | 6. m:. m ~ {t:T| B(t) } Fin({t:T| B(t) }) |
About:
 |  |  |  |  |  |  |  |