Subst tm

lemma subst_tm (der : Typing (Γ ++ ⟨X, .ty σ⟩ :: Δ) t τ) (der_sub : Typing Δ s σ) :    Typing (Γ ++ Δ) (t[X := s]) τ := by  generalize eq : Γ ++ ⟨X, .ty σ⟩ :: Δ = Θ at der  induction der generalizing Γ X  case var σ' _ X' _ _ =>    have : Γ ++ ⟨X, .ty σ⟩ :: Δ ~ ⟨X, .ty σ⟩ :: (Γ ++ Δ) := perm_middle    by_cases eq : X = X'    · #adaptation_note      /--      Moving from `nightly-2025-09-15` to `nightly-2025-10-19`,      I've had to remove the `append_assoc` lemma from grind;      without this `grind` is exploding. This requires further investigation.      -/      grind [→ List.mem_dlookup, weaken_head, Env.Wf.strengthen, -append_assoc]    · grind [Env.Wf.strengthen, => List.perm_dlookup]  case abs => grind [abs (free_union Var), openTm_substTm_var]  case tabs => grind [tabs (free_union Var), openTy_substTm_var]  case let' der _ => grind [let' (free_union Var) (der eq), openTm_substTm_var]  case case der _ _ =>    apply case (free_union Var) (der eq) <;> grind [openTm_substTm_var]  all_goals grind [Env.Wf.strengthen, Ty.Wf.strengthen, Sub.strengthen]