n:
, f:(n
T), i:n. (f{n})[i] = f(i)i:
, E:({...i}Prop).
Thm* E(i)
(k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))a:T, as:T List, i:. i
0 (a.as)[i] = aa:T, as:T List, i:. 0<i i||as|| (a.as)[i] = as[(i-1)]| Rank | Theorem | Name |
| 6 | n:, f:(nT), i:n. (f{n})[i] = f(i) | [select_listify_id] |
| 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] |
| 0 | a:T, as:T List, i:. i0 (a.as)[i] = a | [select_cons_hd] |
| 0 | a:T, as:T List, i:. 0<i i||as|| (a.as)[i] = as[(i-1)] | [select_cons_tl] |