Nuprl - Proof: select upto

i,j:, k:(j-i). upto(i;j)[k] = i+k

By: Assert (d,i,j:, k:d. j-i = d upto(i;j)[k] = i+k)

Generated subgoals:

1 d,i,j:, k:d. j-i = d upto(i;j)[k] = i+k 4 steps

2 1. d,i,j:, k:d. j-i = d upto(i;j)[k] = i+k
i,j:, k:(j-i). upto(i;j)[k] = i+k 1 step

About:

1	`d,i,j:, k:d. j-i = d upto(i;j)[k] = i+k`	4 steps

2	1. `d,i,j:, k:d. j-i = d upto(i;j)[k] = i+k` `i,j:, k:(j-i). upto(i;j)[k] = i+k`	1 step