1. T1 : Type
2. T2 : Type
3. T1 List
4. u : T1
5. v : T1 List
6. bs:T2 List. zip(v;bs)  (T1T2) List
7. T2 List
8. T2
9. v1 : T2 List
10. (Case of v1; nil  nil ; b.bs'  [<u,b> / zip(v;bs')])  (T1T2) List
  zip(v;v1)  (T1T2) List

None

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