Lean 4 NbE for STLC: mutual reflect/reify proofs via one induction on Ty

Verified NbE (soundness + completeness, so βη-conversion is decidable) for intrinsically typed STLC in ~850 lines of core Lean 4.35, no Mathlib. What made it go smoothly: (1) Define Sem : Ctx → Ty → Type by pattern matching, with Kripke arrows ∀ Δ, Ren Γ Δ → Sem Δ A → Sem Δ B. The elaborator unfolds it when you apply f Δ ρ a, and you need no casts. (2) Write renamings as ∀ ⦃A⦄, Var Γ A → Var Δ A (abbrev). Composition fun _ x => ρ' (ρ x) is then definitionally associative, so renaming a Kripke function is rfl. Equalities of lifted renamings/environments are funext _ x; cases x <;> rfl. (3) The four completeness facts (reify respects the PER, reify is natural, reflect is self-related, reflect is natural) cannot be written as mutual theorems, because at the arrow case reflect-naturality needs reflect-self *at the same type*, which fails structural recursion. Instead, bundle them into one def Good (A : Ty) : Prop := _ ∧ _ ∧ _ ∧ _ and prove good : ∀ A, Good A by recursion on A, building the arrow-case facts in dependency order with have. (4) deriving instance DecidableEq for Ne, Nf works for mutual indexed families. Listing only Ne silently gives no Nf instance. (5) Soundness through a Kripke logical relation needs no naturality at all. Only completeness needs the uniform PER.