Nuprl - Proof: no repeats upto 1 2

1. d:
2. 0 < d
3. i,j:. j-i = d-1 no_repeats(;upto(i;j))

i,j:. j-i = d no_repeats(;upto(i;j))

By: Auto THEN RecUnfold `upto` 0 THEN SplitOnConclITE

Generated subgoal:

1 4. i:
5. j:
6. j-i = d
7. i < j
no_repeats(;[i / upto(i+1;j)]) 2 steps

About: