Nuprl - Proof: listify select id 1 1 2 2 2 1

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

1. T : Type
2. T List
3. n :

4. T
5. v : T List
6.

. j+||v|| = n

(

i.v[(i-j)]){j..n

} = v
7. j :

8. j+||v||+1 = n
9. j<n

(

i.v[(i-j-1)]){(j+1)..n

} = v

By:	InstHyp [j+1] 6

Generated subgoal:

1 10. (i.v[(i-(j+1))]){(j+1)..n} = v
(i.v[(i-j-1)]){(j+1)..n} = v
1 step

About:

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