| Rank | Theorem | Name |
| 9 | Thm* ( a inj b) ~ (b!a) | [nsub_inj_factorial_tail] |
| cites the following: |
| 1 | Thm*  m,k:. m = 0    k!m = 1 | [factorial_tail_via_iter_null] |
| 0 | Thm* (A ~ 1)  ( !A) | [card1_iff_inhabited_uniquely] |
| 0 | Thm*  (A) (!(A inj B)) | [inj_from_empty_unique] |
| 4 | Thm* m,k:. 1  m k k!m = k (k-1)!(m-1) | [factorial_tail_via_iter_step_rw] |
| 2 | Thm* a,b: . (a inj b) ~ (b ((a-1) inj (b-1))) | [card_nsub_inj_vs_lopped] |
| 8 | Thm* a,b:. (ab) ~ (ab) | [nsub_mul_rw] |
| 8 | Thm* m,k:. k<m k!m = 0 | [factorial_tail_via_iter_zero] |
| 0 | Thm* (A ~ 0) (A) | [card0_iff_uninhabited] |
| 3 | Thm* ((m inj k)) mk | [inj_typing_imp_le] |