(4steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select zip 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:. i<||zip([u / v];v1)||  zip([u / v];v1)[i] = <[u / v][i],v1[i]>
  i:. 
  i<||zip(v;v1)||+1  [<u,u1> / zip(v;v1)][i] = <[u / v][i],[u1 / v1][i]>
By: UnivCD THEN CaseNat 0 `i'

Generated subgoals:

1 11. i : 
12. i<||zip(v;v1)||+1
13. i = 0
  [<u,u1> / zip(v;v1)][0] = <[u / v][0],[u1 / v1][0]>
1 step
2 11. i : 
12. i<||zip(v;v1)||+1
13. i = 0
  [<u,u1> / zip(v;v1)][i] = <[u / v][i],[u1 / v1][i]>
1 step

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

(4steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc