Nuprl - Proof: no repeats upto 1 1

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

By: Auto THEN RecUnfold `upto` 0 THEN SplitOnConclITE

Generated subgoal:

1 1. i:
2. j:
3. j-i = 0
4. ji
no_repeats(;nil) 1 step

About: