Nuprl - Proof: upto int wf

i,j:. upto(i;j) List

By: Assert (d:, i,j:. j-i = d upto(i;j) List)

Generated subgoals:

1 d:, i,j:. j-i = d upto(i;j) List 2 steps

2 1. d:, i,j:. j-i = d upto(i;j) List
i,j:. upto(i;j) List 3 steps

About:

1	`d:, i,j:. j-i = d upto(i;j) List`	2 steps

2	1. `d:, i,j:. j-i = d upto(i;j) List` `i,j:. upto(i;j) List`	3 steps