Nuprl - Proof: int lower ind 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: int lower ind 1 1 1

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>j

E(k)

E(j)

By:	Decide: j = i

Generated subgoals:

1 8. j = i
E(j)
1 step

2 8. j = i
E(j)
2 steps

About:

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