1. i : 
2. j : {i+1...}
3. E : {i..j}Prop
4. E(i)
5. k:{(i+1)..j}. E(k-1)  E(k)
  j@0:{i..j}. (k:{i..j}. k<j@0  E(k))  E(j@0)

1

6. j@0 : {i..j} 7. k:{i..j}. k<j@0  E(k)   E(j@0)

5 steps

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