b inj
b) ~ (b!)1) 
(
!
A)
(A) 
(!(A inj B))
a,b:
. (a inj b) ~ (b
((a-1) inj (b-1)))a,b:. (ab) ~ (a
b)k:. k! = k(k-1)! | Rank | Theorem | Name |
| 9 | b inj b) ~ (b!) | [nsub_inj_factorial2] |
| cites the following: | ||
| 0 | 1) (!A) | [card1_iff_inhabited_uniquely] |
| 0 | (A) (!(A inj B)) | [inj_from_empty_unique] |
| 2 | a,b:. (a inj b) ~ (b((a-1) inj (b-1))) | [card_nsub_inj_vs_lopped] |
| 8 | a,b:. (ab) ~ (ab) | [nsub_mul_rw] |
| 5 | k:. k! = k(k-1)! | [factorial_via_intseg_step_rw] |