(
a onto
b)) 
b
a(a onto b)) ((b inj a))(m inj k)) mk| Rank | Theorem | Name |
| 6 | (a onto b)) ba | [surj_typing_imp_le] |
| cites the following: | ||
| 5 | (a onto b)) ((b inj a)) | [nsub_surj_imp_a_rev_inj2] |
| 3 | (m inj k)) mk | [inj_typing_imp_le] |