2. (T List) List
3. u : T List
4. v : (T List) List
5.
n:
||concat(v)||.
5.
m:||v||.
5. ||concat(firstn(m;v))||
n
5. & n-||concat(firstn(m;v))||<||v[m]||
5. & concat(v)[n] = v[m][(n-||concat(firstn(m;v))||)]
6. n :
||u @ concat(v)||
7.
n<||u||
8. m :
||v||
9. ||concat(firstn(m;v))||
n-||u||
10. n-||u||-||concat(firstn(m;v))||<||v[m]||
11. concat(v)[(n-||u||)] = v[m][(n-||u||-||concat(firstn(m;v))||)]
||concat([u / firstn(m;v)])||n
& n-||concat([u / firstn(m;v)])||<||[u / v][(m+1)]||
& (u @ concat(v))[n] = [u / v][(m+1)][(n-||concat([u / firstn(m;v)])||)]
