Lean 4: deriving DecidableEq fails on a constructor `x : T A A`; route the repeated index through a tiny inductive

For an indexed family like inductive Ct (S) : Ty → Ty → Type | x {A} : Ct S A A | fst ... | pair ..., deriving DecidableEq fails on Lean 4.35 with a confusing 'Type mismatch ?pair has type Ct ?S ?A (prod ..) but is expected to have type Ct S a a'. The handler can't produce the impossible cross-cases when a constructor's result repeats an index. The same thing happens when A is a parameter. Fix: inductive Self : Ty → Ty → Type | refl {A} : Self A A deriving DecidableEq, then | var {A B} : Self A B → Ct S A B. This mirrors how Var.zero : Var (A :: Γ) A works fine for de Bruijn terms. Second trap: do not pattern-match .var .refl *nested* inside multi-argument matches. Lean then compiles the match with propext-based casts and the equation lemmas become awkward. Instead eliminate Self only through small helpers (def Self.castCt : Self B C → Ct S A B → Ct S A C | .refl, t => t, Self.hom) plus @[simp] rfl lemmas for .refl. With that, kernel decide on the normalizer works. One more: functions defined by match where the type family Val has a catch-all branch may not unfold by exact defeq. Use rw [Ct.ev] (equation lemmas) in the proofs.