Nuprl - Proof: int upper ind 1 1 1 2

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

1. i :

2. E : {i...}

Prop
3. E(i)
4.

k:{i+1...}. E(k-1)

E(k)
5. j : {i...}
6.

k:{i...}. k<j

E(k)
7.

j = i

E(j)

By:	(BackThru 4) THEN (BackThru 6)

Generated subgoals:

None

About:

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