New module Erase for dealing with erased and resurrected values

[jespercockx]

No description provided.

[flupe]

Same comment as some other PR, Erase and Erased should be mapped to () in agda2hs itself.

[flupe]

Rebased on #254 . Now using Haskell.Extra.Erase does not generate Haskel/Extra/Erase.hs, all the definitions are inlined or mapped to ().

[flupe]

I think I remember Σ0 being moved to some other module but cannot seem to find any trace of it. Apologies if I overwrote some of your changes...

[jespercockx]

I think I remember Σ0 being moved to some other module but cannot seem to find any trace of it. Apologies if I overwrote some of your changes...

I moved it to Haskell.Extra.Refinement because it didn't really have much to do with erasure per se. But it doesn't really matter too much.

[jespercockx]

Oops, @flupe I think I accidentally undid your change while fixing the merge conflict. Could you rebase it and push it again?