grind heterogeneous injectivity vs. parameters

[nomeata]

I was hoping that since fixing #11449 grind would solve

example
 (a b c d : Nat)
 (h1 : c.succ < a)
 (h2 : d.succ < b)
 (hab : a = b)
 (hcd : @Fin.mk a c.succ h1 ≍ @Fin.mk b d.succ h2) : 
 c = d := by grind

but it doens’t handle that yet. This comes up in #11512.

In #11449 we had a HEq between constructors with different indices, but here it is a parameter that’s different. So far, the Fin.mk.noConfusion is not heterogenenous in the parameter:

Fin.mk.noConfusion.{u} {n : Nat} {P : Sort u} {val : Nat} {isLt : val < n} {val' : Nat} {isLt' : val' < n}
  (eq : ⟨val, isLt⟩ = ⟨val', isLt'⟩) (k : val = val' → P) : P

I wonder Fin.mk.noConfusion should just accept propositional equalities between parameters, just like with indices.

Versions

nightly-2025-12-08

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

I’ll investigate

I wonder Fin.mk.noConfusion should just accept propositional equalities between parameters, just like with indices.

first, this may solve this issue without changing gind.