Nuprl - Proof: select firstn 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select firstn 1 1 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. u : T
8. v : T List
9. n

||v||+1
10. i :

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

By:	Decide (i = 0)

Generated subgoals:

1 11. i = 0
(u.firstn(n-1;v))[i] = (u.v)[i]
1 step

2 11. i = 0
(u.firstn(n-1;v))[i] = (u.v)[i]
2 steps

About:

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

1	11. i = 0 (u.firstn(n-1;v))[i] = (u.v)[i]	1 step
2	11. i = 0 (u.firstn(n-1;v))[i] = (u.v)[i]	2 steps