as:T List, n:{0...||as||}, i:
n. firstn(n;as)[i] = as[i]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)]| Theorem | Name |
| as:T List, n:{0...||as||}, i:n. firstn(n;as)[i] = as[i] | [select_firstn] |
| cites the following: | |
| a:T, as:T List, i:. i0 (a.as)[i] = a | [select_cons_hd] |
| a:T, as:T List, i:. 0<i i||as|| (a.as)[i] = as[(i-1)] | [select_cons_tl] |