Nuprl - Proof: int lower ind 1 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

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)
8. j = i

E(j)

By:	Rewrite by j = i {...i}

Generated subgoals:

None

About:

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