Nuprl - Proof: mklist select 2 1 2 1

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

1. T : Type
2. n :

3. 0<n
4.

f:(

(n-1)

T), i:

(n-1). mklist(n-1;f)[i] = f(i)
5. f :

T
6.

(n-1). mklist(n-1;f)[i] = f(i)
7.

n = 0
8. i :

(mklist(n-1;f) @ [(f(n-1))])[i] = f(i)

By:	Decide (i<n-1)

Generated subgoals:

1 9. i<n-1
(mklist(n-1;f) @ [(f(n-1))])[i] = f(i)
3 steps

2 9. i<n-1
(mklist(n-1;f) @ [(f(n-1))])[i] = f(i)
2 steps

About:

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

1	9. i<n-1 (mklist(n-1;f) @ [(f(n-1))])[i] = f(i)	3 steps
2	9. i<n-1 (mklist(n-1;f) @ [(f(n-1))])[i] = f(i)	2 steps