Issue in !4#2409: index is not a variable

Stream: mathlib4

[Arien Malec]

I have !4#2409 (Data.QPF.Multivariate.Fix) down to a single error, for induction h where the error is one I haven't seen:

index in target's type is not a variable (consider using the `cases` tactic instead)
  MvPFunctor.wMk (P F) a₀ f'₀ f₀

(using cases leads to:

dependent elimination failed, failed to solve equation
  (fun i => (f₀ i).fst) = fun i => (f₀✝ i).fst

and we need the ih anyway).