Nuprl - Proof: zip length 1

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

1. T1 : Type
2. T2 : Type
3. T1 List
4. T2 List
5. T2
6. v : T2 List
7. ||zip(nil;v)||

||nil|| & ||zip(nil;v)||

||v||

0 & 0

||v||+1

By:

Thin -1

Generated subgoals:

None

About:

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