Make trivial instances explicit

Merged Maxime Dénès requested to merge maximedenes/stdpp:instance-nobody-open-proof into master

This is in preparation for coq/coq#9274.

Should be backward compatible but that remains to be tested.

Merge request reports