`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.

This has the following advantages:

• We need fewer adhoc Hint Extern instances for the proof mode, we can just use Unify.
• We can consistently use the refine unification algorithm when trying to unify a hypothesis/conclusion of a lemma/wand to the goal. This is currently only done by iAssumption, but not by iFrame or iApply.
• It might allow us to use Typeclasses Opaque for all std++ operational type classes. As described in !914 (comment 91480), this is currently impossible.

We could probably do some bikeshedding about the name or other implementation aspects. But I might make sense to first check out the performance impact and whether it breaks anything in the reverse dependencies. So @jung could you run timing CI, please.