Nuprl - Proof: int seg ind 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. 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)

E(n)

By:	Decide (n = i)

Generated subgoals:

1 8. n = i
E(n)
2 steps

2 8. n = i
E(n)
1 step

About:

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