Nuprl - Proof: upto wf

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

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

Generated subgoals:

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

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

About:

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

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