Nuprl - Proof: unzip zip 1

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

1. T1 : Type
2. T2 : Type
3. T1 List
4. u : T1
5. v : T1 List
6.

bs:T2 List. ||v|| = ||bs||

unzip(zip(v;bs)) = <v,bs>
7. T2 List
8. u1 : T2
9. v1 : T2 List
10. ||[u / v]|| = ||v1||

unzip(zip([u / v];v1)) = <[u / v],v1>

||v||+1 = ||v1||+1

<[u / map(

p.1of(p);zip(v;v1))],[u1 / map(

p.2of(p);zip(v;v1))]>

<[u / v],[u1 / v1]>

By:	((Analyze 0) THEN (InstHyp [v1] 6) THEN (Unfold `unzip` -1) (THEN ((ApFunToHypEquands `z' (z.1) (T1 List) -1) (THEN ((Reduce -1) (THEN ((ApFunToHypEquands `z' (z.2) (T2 List) -2) (THEN ((Reduce -1)) THEN Analyze THEN Analyze THEN Try (Complete Auto)

Generated subgoals:

None

About:

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