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])
6. T List
  [u / v]  nil
  
  ||[u / v]||||nil|| & (i:. i<||[u / v]||  [u / v][i] = nil[i])

1	7. [u / v]  nil   ||v||+10 & (i:. i<||v||+1  [u / v][i] = nil[i])	2 steps
2	7. ||v||+10 & (i:. i<||v||+1  [u / v][i] = nil[i])   [u / v]  nil	1 step

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