m,n:
, f:({m..n
}
T). n<m 
||f{m..n}|| = n-mi:, E:({...i}Prop).
Thm* E(i)
(k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))| Rank | Theorem | Name |
| 6 | m,n:, f:({m..n}T). n<m ||f{m..n}|| = n-m | [listify_length] |
| cites the following: | ||
| 5 | i:, E:({...i}Prop).
Thm* E(i) (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k)) | [int_lower_ind] |