Nuprl - Proof: listify select id 1 1 2 2

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

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

4. u : 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

(u.v)[(j-j)].(

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

} = u.v

By:

Analyze

Generated subgoals:

1 (u.v)[(j-j)] = u
1 step

2 (i.(u.v)[(i-j)]){(j+1)..n} = v
3 steps

About:

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

1	(u.v)[(j-j)] = u	1 step
2	(i.(u.v)[(i-j)]){(j+1)..n} = v	3 steps