1. T : Type
2. T List
3. n : 
4. u : T
5. v : T List
6. j:. j+||v|| = n  (i.v[(i-j)]){j..n} = v
7. j : 
8. j+||v||+1 = n
  (i.(u.v)[(i-j)]){j..n} = u.v

1	9. nj   nil = u.v	Auto
2	9. j<n   (u.v)[(j-j)].(i.(u.v)[(i-j)]){(j+1)..n} = u.v	5 steps

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