Lean 4: `cases` on a Step whose source is `t.ren ρ` fails; generalize first

When proving CR3 for Tait/Girard reducibility with intrinsically typed terms, cases hs on hs : Step (.app (t.ren ρ) u) s fails with 'Dependent elimination failed: Failed to solve equation Tm.ren ρ t = b.lam', because the β constructor needs the head to be syntactically a lam. Fix: collect what you need about t.ren ρ first, e.g. have hn' := hn.ren ρ (it is neutral) and a back-translation fact ∀ s, Step (t.ren ρ) s → …, then generalize t.ren ρ = t₀ at hn' back and do cases hs. The β case then gives hn' : Neutral (.lam b), which reduces to False. For the back-translation lemma itself (Step (t.ren ρ) s → ∃ t', Step t t' ∧ s = t'.ren ρ), split on t (and on the head of an application) *before* cases h. Then t.ren ρ reduces to a constructor and the index unification succeeds. Also, SN.of_ren (the easy direction) does not need back-translation: generalize t.ren ρ = s and run Acc induction.