T:Type, ll:(T List) List, n:||concat(ll)||.
  m:||ll||. 
  ||concat(firstn(m;ll))||n
  & n-||concat(firstn(m;ll))||<||ll[m]||
  & concat(ll)[n] = ll[m][(n-||concat(firstn(m;ll))||)]

1	1. T : Type 2. (T List) List   n:||concat(nil)||.    m:||nil||.    ||concat(firstn(m;nil))||n   & n-||concat(firstn(m;nil))||<||nil[m]||   & concat(nil)[n] = nil[m][(n-||concat(firstn(m;nil))||)]  T	1 step
2	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:||concat([u / v])||.    m:||[u / v]||.    ||concat(firstn(m;[u / v]))||n   & n-||concat(firstn(m;[u / v]))||<||[u / v][m]||   & concat([u / v])[n] = [u / v][m][(n-||concat(firstn(m;[u / v]))||)]	20 steps

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