Actually prove that Set’s have linear height
Actually prove that Set’s have linear height

it was easy to show that the size has a lower bound that is exponential
in the height was easy. But then turning the equation around, using
Coq’s lemmas and staying within `Z`, was frustratingly much more work.

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