perf: do not instantiate constant types in `isPropQuick`, `isProofQuick` and `isTypeQuick`

For a constant head, these predicates instantiated the universe parameters of the constant's whole type, usually with fresh level metavariables, so the instantiation cache rarely hit; `isDefEqProofIrrel` calls `isProofQuick` on every `isDefEq` problem. They only inspect the binder structure of that type, the levels of the `Sort`s they reach and the levels of constants they recurse into. They now walk the uninstantiated type and substitute just those levels (`LevelSubst`), with `Level.instantiateParams`, which is what `Expr.instantiateLevelParams` applies to each level. Level instantiation does not change the structure of an expression, so the results are the same; the types of free variables and metavariables are not substituted, as before. A differential check against the previous implementation over every 7th constant of `import Lean`, 8 level patterns (including the constant's own parameter names, swapped, and assigned and unassigned level metavariables) and arities 0 to 8 found no disagreement in 4.4 M calls.

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