a,b:
. (a inj
b) ~ (b
((a-1) inj (b-1)))a:, b:, f:(a inj b). f 
(a-1) inj {x:b| 
x = f(a-1) }a:, b:, j:b, f:((a-1) inj {x:b| x = j }).
Thm* (
i.if i=
a-1 j else f(i) fi) a inj bk:, j:k. {i:k| i = j } ~ (k-1)| Rank | Theorem | Name |
| 2 | a,b:. (a inj b) ~ (b((a-1) inj (b-1))) | [card_nsub_inj_vs_lopped] |
| cites the following: | ||
| 0 | a:, b:, f:(a inj b). f (a-1) inj {x:b| x = f(a-1) } | [nsub_inj_lop_typing] |
| 0 | a:, b:, j:b, f:((a-1) inj {x:b| x = j }).
Thm* ( i.if i=a-1 j else f(i) fi) a inj b | [nsub_inj_fill_typing] |
| 1 | k:, j:k. {i:k| i = j } ~ (k-1) | [nsub_delete_rw] |