grind: no subsingleton elimination for `DecidablePred` instances

grind canonicalises Decidable instances, so it identifies terms differing only in one. It does not do the same for instances at a pi type such as DecidablePred p, so terms differing only in a DecidablePred are never identified.

opaque P : Nat → Prop
opaque Q : Prop

-- succeeds: the instance argument is a `Decidable`
opaque f (p : Prop) [Decidable p] : Nat
example (i₁ i₂ : Decidable Q) : @f Q i₁ = @f Q i₂ := by grind

-- fails: the instance argument is a `DecidablePred`, i.e. a pi into `Decidable`
opaque g (p : Nat → Prop) [DecidablePred p] : Nat
example (i₁ i₂ : DecidablePred P) : @g P i₁ = @g P i₂ := by grind

-- the fact `grind` needs is available
example (i₁ i₂ : DecidablePred P) : i₁ = i₂ := Subsingleton.elim _ _

grind reports the cause itself:

[grind] Issues
  [issue] failed to canonicalize instance
        i₁
      synthesized instance is not definitionally equal
        i₂

This is long-standing rather than a regression: it reproduces identically on nightly-2026-08-16, nightly-2026-08-13, nightly-2026-08-12 and v4.34.0-rc1.

It surfaced on Mathlib's nightly-testing branch because a proof that used to work now needs it. In Mathlib/Dynamics/PeriodicPts/Lemmas.lean, minimalPeriod_eq_sInf_n_pos_IsPeriodicPt reduces to two copies of the same dite differing only in the DecidablePred handed to Nat.find, instDecidableAnd .. (IsPeriodicPt.instDecidableOfDecidableEq ..) on one side and Classical.propDecidable on the other. grind closed that until nightly-2026-08-13, but only as a side effect of cutsat's ToInt component internalising the term; feat: homomorphisms for grind (#14727) removed that route. So the Mathlib breakage is not a bug in #14727, but closing this gap would fix that proof properly.

Reproduce the issue with the Decidable and DecidablePred examples in the report, then trace grind's instance-canonicalization path to where pi-valued instances are handled. Use the Mathlib/Dynamics/PeriodicPts/Lemmas.lean breakage as a regression case; done means the DecidablePred equality example and the affected Mathlib proof close without relying on the removed ToInt path.