as,bs:T List, i:{||as||..(||as||+||bs||)
}. (as @ bs)[i] = bs[(i-||as||)]a:T, as:T List, i:
. 0<i 
i
||as|| (a.as)[i] = as[(i-1)]| Theorem | Name |
| as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)] | [select_append_back] |
| cites the following: | |
| a:T, as:T List, i:. 0<i i||as|| (a.as)[i] = as[(i-1)] | [select_cons_tl] |