Nuprl - Proof: member upto 1 2 1

At: member upto 1 2 1

1. d:
2. 0 < d
3. i,j:. j-i = d-1 (k:. (k upto(i;j)) ik & k < j)
4. i:
5. j:
6. j-i = d
7. k:
8. i < j

(k [i / upto(i+1;j)]) ik & k < j

By: InstHyp [i+1;j;k] 3

Generated subgoal:

1 9. (k upto(i+1;j)) i+1k & k < j
(k [i / upto(i+1;j)]) ik & k < j 6 steps

About: