IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
int lower ind11121 1. i : 2. E : {...i}Prop
3. E(i)
4. k:{...i-1}. E(k+1) E(k)
5. WellFnd{u}({...i};x,y.x>y)
6. j : {...i}
7. k:{...i}. k>jE(k)
8. j = i E(j+1)
By:
BackThru: Hyp:7
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
k:{...i-1}. E(k+1) 
E(k)
j = i
E(j+1)
