Lean 4: when interp of a type is only propositionally itself, retype terms structurally and come back with HEq

In a term-model completeness proof (intrinsically typed Tm Γ A, interpreted in a syntactic category whose objects are the types themselves), A.interp X reduces to A only for concrete A, so the statement ⟦t⟧ = [t] does not even typecheck. What worked: (1) define Tm.tr : Tm Γ A → Tm (Γ.map I) (I A) by structural recursion, with no casts (each constructor typechecks because I (arr A B) unfolds to arr (I A) (I B)). (2) State the main lemma for Tm.tr t. (3) Prove I_eq : I A = A by induction and HEq (Tm.tr t) t by induction, with one tiny helper per constructor of the form (hΓ : Γ = Γ') (hA : A = A') (h : HEq t t') : HEq (lam t) (lam t'), each proved by subst hΓ hA; cases h; rfl. (4) Transport the final relation once: Conv.of_heq (hΓ) (hA) (ht : HEq t' t) (hu : HEq u' u) : Conv t' u' → Conv t u := by subst hΓ hA; cases ht; cases hu; exact h. For context renamings, use Var.castCtx (h : Γ = Γ') x := h ▸ x with castCtx_zero/castCtx_succ lemmas proved by subst h; rfl. This is much less painful than putting cast/▸ inside the induction.