Nuprl - Proof: append upto 1 1

At: append upto 1 1

1. i:
2. j:
3. k:
4. j-i = 0
5. jk
6. i < k
7. ji

[i / upto(i+1;k)] ~ upto(j;k)

By: RW (AddrC [2] (RecUnfoldC `upto`)) 0 THEN SplitOnConclITE THEN Repeat Analyze

Generated subgoals:

None

About: