| Entry | Value |
|---|---|
| Name | unzip_def |
| Conclusion | unzip = foldr (\(x,y) (xs,ys). CONS x xs,CONS y ys) ([],[]) |
| Constructive Proof | Yes |
| Axiom | N|A |
| Classical Lemmas | N|A |
| Constructive Lemmas | N|A |
| Contained Package | list-zip-def |
| Comment | Standard HOL library retrieved from OpenTheory |