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

By:	BackThruLemmaWithUnfolds Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x<y) [`wellfounded`]

1

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

6 steps

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