Nuprl - Proof: select listify id 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select listify id 1

1. T : Type
2. n :

3. f :

T
4. i :

(f{

n})[i] = f(i)

By:	Assert (j:{...n}. 0j (i:{j..n}. (f{j..n})[(i-j)] = f(i))) THENA Thin 4

Generated subgoals:

1   j:{...n}. 0j  (i:{j..n}. (f{j..n})[(i-j)] = f(i))
9 steps

2 5. j:{...n}. 0j  (i:{j..n}. (f{j..n})[(i-j)] = f(i))
  (f{n})[i] = f(i)
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	j:{...n}. 0j (i:{j..n}. (f{j..n})[(i-j)] = f(i))	9 steps
2	5. j:{...n}. 0j (i:{j..n}. (f{j..n})[(i-j)] = f(i)) (f{n})[i] = f(i)	1 step