fix: `isDefEq` for constants with different universe parameters
This PR fixes a bug at the definitional equality test (`isDefEq`). At
unification constraints of the form `c.{u} =?= c.{v}`, it was not
trying to unfold `c`. This bug did not affect the kernel.
closes #6117
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).