1. T : Type
2. T List
3. u : T
4. v : T List
5. n:{0...||v||}, i:(||v||-n). nth_tl(n;v)[i] = v[(i+n)]
  n:{0...||v||+1}, i:(||v||+1-n). nth_tl(n;u.v)[i] = (u.v)[(i+n)]

1	6. n : {0...||v||+1} 7. i : (||v||+1-n) 8. n0   (u.v)[i] = (u.v)[(i+n)]	2 steps
2	6. n : {0...||v||+1} 7. i : (||v||+1-n) 8. 0<n   nth_tl(n-1;v)[i] = (u.v)[(i+n)]	2 steps

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