perf: cache universe instantiations of constants per level list

This PR makes `Core.instantiateTypeLevelParams` and `Core.instantiateValueLevelParams` cache instantiations by constant name and universe levels. They cached only the most recent instantiation of each constant, so a constant used at alternating universe levels, such as `Eq` or `HAdd.hAdd` at different sorts, instantiated its whole type or value again on each switch.

The cached result was already assumed to depend only on the name and the levels. One cache-dependent case can now differ: a call with `allowOpaque := false` on a theorem or opaque constant whose value was cached by an `allowOpaque := true` call (such as those in `Meta.Transform`, or from `deltaExpand` with `allowOpaque := true`) returns that value where it would throw unless its levels were the most recently cached ones; the previous code already skipped the check on a hit.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>