Avoid relying on implicit instance generalization, and name some instances.

Fix in preparation for https://github.com/coq/coq/pull/13188

I didn't name the Forall2 instances, since I could not come up with a good naming scheme. So, I just used the ∀.

There are probably plenty of other unnamed instances, but I would prefer defer naming them.