fix: avoid `mkEqMP` This PR ensures that `grind` does not use `mkEqMP`. It often triggered type errors because `grind` uses the `[reducible]` transparency setting by default. Increasing the transparency setting to default was another possible, but less efficient fix.
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).