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

None

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