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

1

4. n1 :  5. m1 : {n1...} 6. a2 : {n1..m1}T 7. <n1,m1,a2>.l = i & <n1,m1,a2>.u = j 8. m : {i..j} 9. n : {m..j}   <m,n,2of(2of(<n1,m1,a2>))>  n:m:{n...}{n..m}T

2 steps

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