Nuprl - Proof: zip unzip 1 1

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

1. T1 : Type
2. T2 : Type
3. (T1

T2) List
4. u : T1

T2
5. v : (T1

T2) List
6. zip(map(

p.1of(p);v);map(

p.2of(p);v)) = v

[<1of(u),2of(u)> / zip(map(

p.1of(p);v);map(

p.2of(p);v))] = [u / v]

By:	Analyze -3 THEN Reduce 0 THEN Analyze

Generated subgoals:

None

About:

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