Nuprl - Proof: select zip 1 1

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

1. T1 : Type
2. T2 : Type
3. T1 List
4. u : T1
5. v : T1 List
6.

bs:T2 List, i:

. i<||zip(v;bs)||

zip(v;bs)[i] = <v[i],bs[i]>
7. T2 List
8. u1 : T2
9. v1 : T2 List
10.

. i<||zip([u / v];v1)||

zip([u / v];v1)[i] = <[u / v][i],v1[i]>
11. i :

12. i<||zip(v;v1)||+1
13. i = 0

[<u,u1> / zip(v;v1)][0] = <[u / v][0],[u1 / v1][0]>

By:

Reduce 0

Generated subgoals:

None

About:

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