1. T : Type
2. T List
3. u : T
4. v : T List
5. l2:T List. v  l2  ||v||||l2|| & (i:. i<||v||  v[i] = l2[i])
  l2:T List. 
  [u / v]  l2
  
  ||[u / v]||||l2|| & (i:. i<||[u / v]||  [u / v][i] = l2[i])

1	6. T List   [u / v]  nil      ||[u / v]||||nil|| & (i:. i<||[u / v]||  [u / v][i] = nil[i])	4 steps
2	6. T List 7. u1 : T 8. v1 : T List 9. [u / v]  v1 9.  9. ||[u / v]||||v1|| & (i:. i<||[u / v]||  [u / v][i] = v1[i])   [u / v]  [u1 / v1]      ||[u / v]||||[u1 / v1]||   & (i:. i<||[u / v]||  [u / v][i] = [u1 / v1][i])	12 steps

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