Nuprl - Proof: int seg ind 1 1 1 1 2

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

1. i :

2. j : {i+1...}
3. E : {i..j

}

Prop
4. E(i)
5.

k:{(i+1)..j

}. E(k-1)

E(k)
6. n : {i..j

}
7.

k:{i..j

}. k<n

E(k)
8.

n = i

E(n)

By:	(BackThru 5) THEN (BackThru 7)

Generated subgoals:

None

About:

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