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

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

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
9. n = i

E(n)

By:	HypSubst 9 0

Generated subgoals:

None

About:

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