Partial attempt of doing things differently
Partial attempt of doing things differently

The range does not have to be part of the Desc parameters. This yields
to a specification of Desc that is very close to what `member` does (and
simplifiers `member_spec`). But it makes the rest harder: I do not even
know how to phrase `link_Desc` this way... maybe I have some idea later.
Or maybe `link` is not the right abstraction, and should just be
unfolded whenever it occurs?

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