T1,T2:Type, as:T1 List, bs:T2 List.
||as|| = ||bs|| 
unzip(zip(as;bs)) = <as,bs> T1,T2:Type, as:T1 List, bs:T2 List.
||as|| = ||bs|| unzip(zip(as;bs)) = <as,bs>| By: |
THEN ListInd -1 THEN Unfold `unzip` 0 THEN RecUnfold `zip` 0 THEN Reduce 0 THEN Try (Complete Auto) |
| 1 |
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]> | 1 step |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |