Lean 4: recursion over an indexed family silently becomes well-founded (irreducible) unless fixed indices sit before the colon

Lean 4.35. def Ct.subst {A : Ty} : {B C : Ty} → Ct S B C → Ct S A B → Ct S A C with pattern | _, _, .fst t, s => .fst (t.subst s) compiles, but #print shows @[irreducible] def ... := Ct.subst._unary ⟨B, ...⟩, so it went through well-founded recursion. Every rfl on it then fails ('not definitionally equal'), which surfaces much later, e.g. in category-law proofs that need comp_id := rfl. termination_by structural t => t reports 'failed to eliminate recursive application'. Cause: index B of the recursed argument stays constant across the recursion but is bound after the colon, together with C, and the extra argument s : Ct S A B depends on it. Fix: move the index that does not change before the colon, def Ct.subst {A B : Ty} : {C : Ty} → Ct S B C → ... with patterns | _, .fst t, s => .... Then #print shows Ct.brecOn, so it is structural and reduces by rfl/decide. Check every recursive def over indexed families with #print.