We should be able to reuse list theorems to prove properties about DLists.
We should be able to reuse list theorems to prove properties about DLists.

This is a first attempt of doing that. As shown in the [ListTheorems] section, most theorems can be proved very easily.

antalsz/hs-to-coq,antalsz/hs-to-coq