n:
, f:(n
T), i:n. mklist(n;f)[i] = f(i)as,bs:T List, i:||as||. (as @ bs)[i] = as[i]n:, f:(nT). ||mklist(n;f)|| = n 
as,bs:T List, i:{||as||..(||as||+||bs||)
}. (as @ bs)[i] = bs[(i-||as||)]| Rank | Theorem | Name |
| 2 | n:, f:(nT), i:n. mklist(n;f)[i] = f(i) | [mklist_select] |
| cites the following: | ||
| 1 | as,bs:T List, i:||as||. (as @ bs)[i] = as[i] | [select_append_front] |
| 1 | n:, f:(nT). ||mklist(n;f)|| = n | [mklist_length] |
| 1 | as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)] | [select_append_back] |