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.

theories/base.v

@@ -183,6 +183,7 @@ Definition tc_to_bool (P : Prop)
 
 (** Throughout this development we use [stdpp_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
+Declare Scope stdpp_scope.
 Delimit Scope stdpp_scope with stdpp.
 Global Open Scope stdpp_scope.