Drop support for Coq 8.8 and 8.9

This lets us clean up some little things (see this MR), and it enables some major improvements to gmap and Qp by relying on definitionally proof-irrelevant propositions.

I asked last evening on Mattermost if anyone still uses std++ with such old versions of Coq. So far, nobody responded, but it has been less than 24h. On the other hand, such users can just stick to std++ 1.4.0.