1. T1 : Type
2. T2 : Type
3. T1 List
4. u : T1
5. v : T1 List
6. bs:T2 List. ||v|| = ||bs||  ||zip(v;bs)|| = ||v||
7. T2 List
8. T2
9. v1 : T2 List
10. ||[u / v]|| = ||v1||  ||zip([u / v];v1)|| = ||[u / v]||
11. ||v||+1 = ||v1||+1
  ||zip(v;v1)|| = ||v||  

None

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