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.

But let's wait a couple of days so people can respond.

It's been a week now since I asked in Mattermost, and noone spoke up.

Let's merge.

merged

mentioned in commit 7f934a94