f:(
m
k). Inj(m; k; f)) 
m
k(m+1); (k+1); f) Inj(m; k; Replace value k by f(m) in f)| Rank | Theorem | Name |
| 2 | f:(mk). Inj(m; k; f)) mk | [inj_imp_le] |
| cites the following: | ||
| 1 | (m+1); (k+1); f) Inj(m; k; Replace value k by f(m) in f) | [delete_fenum_value_is_inj] |