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

1

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

4 steps

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