Make trivial instances explicit

This is in preparation for coq/coq#9274.
7 jobs for ci/maximedenes/instance-nobody-open-proof in 20 minutes and 26 seconds
Status Name Job ID Coverage
  Build
passed build-coq.8.7.1 #22179
fp

00:05:56

passed build-coq.8.7.2 #22178
fp

00:05:58

passed build-coq.8.8.0 #22177
fp-timing

00:05:07

passed build-coq.8.8.1 #22176
fp

00:06:18

passed build-coq.8.8.2 #22175
fp

00:06:17

passed build-coq.8.9.dev #22174
fp-timing

00:06:14

passed build-coq.dev #22173
fp

00:20:25