'a:S, n:
, l:'a List. n<||l|| 
el(n,l) = l[n]a:T, as:T List, i:
. i
0 cons(a; as)[i] = aa:T, as:T List, i:. 0<i i||as|| cons(a; as)[i] = as[(i-1)]| Theorem | Name |
| 'a:S, n:, l:'a List. n<||l|| el(n,l) = l[n] | [hel_nuprl] |
| cites the following: | |
| a:T, as:T List, i:. i0 cons(a; as)[i] = a | [select_cons_hd] |
| a:T, as:T List, i:. 0<i i||as|| cons(a; as)[i] = as[(i-1)] | [select_cons_tl] |