1. T : Type
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))||)]
  n:||u @ concat(v)||. 
  m:(||v||+1). 
  ||concat(firstn(m;[u / v]))||n
  & n-||concat(firstn(m;[u / v]))||<||[u / v][m]||
  & (u @ concat(v))[n] = [u / v][m][(n-||concat(firstn(m;[u / v]))||)]

1	6. n : ||u @ concat(v)|| 7. n<||u||   m:(||v||+1).    ||concat(firstn(m;[u / v]))||n   & n-||concat(firstn(m;[u / v]))||<||[u / v][m]||   & (u @ concat(v))[n] = [u / v][m][(n-||concat(firstn(m;[u / v]))||)]	4 steps
2	6. n : ||u @ concat(v)|| 7. n<||u||   m:(||v||+1).    ||concat(firstn(m;[u / v]))||n   & n-||concat(firstn(m;[u / v]))||<||[u / v][m]||   & (u @ concat(v))[n] = [u / v][m][(n-||concat(firstn(m;[u / v]))||)]	14 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html