Nuprl - Proof: select firstn 1 1 1 2 1

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

1. T : Type
2. n :

3. 0<n
4.

as:T List. n-1

||as||

(

(n-1). firstn(n-1;as)[i] = as[i])
5. 0<n
6. T List
7. T
8. v : T List
9. n

||v||+1
10. i :

n
11.

i = 0

firstn(n-1;v)[(i-1)] = v[(i-1)]

By:	BackThru 4

Generated subgoals:

None

About:

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