1. T : Type
2. i : 
3. j : {i...}
4. a : [T]Array 
5. a.l = i & a.u = j
6. m : 
  a[++m]  [T]Array 

1

4. n :  5. m1 : {n...} 6. a2 : {n..m1}T 7. <n,m1,a2>.l = i & <n,m1,a2>.u = j 8. m :    <(<n,m1,a2>.l+m),(<n,m1,a2>.u+m),(j.<n,m1,a2>[(j-m)])>    n:m:{n...}{n..m}T

5 steps

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