k inj
k) =ext (k onto k)
(m inj k)) 
m
k
(x:T. Q(x)) (
x:T. Q(x))k:, j:k. {i:k| i = j } ~ (k-1)(a onto b)) ba| Rank | Theorem | Name |
| 7 | k inj k) =ext (k onto k) | [nsub_inj_exteq_nsub_surj] |
| cites the following: | ||
| 3 | (m inj k)) mk | [inj_typing_imp_le] |
| 1 | (x:T. Q(x)) (x:T. Q(x)) | [not_over_exists_imp] |
| 1 | k:, j:k. {i:k| i = j } ~ (k-1) | [nsub_delete_rw] |
| 6 | (a onto b)) ba | [surj_typing_imp_le] |