Typing preservation

lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing Γ t' τ := by  induction der generalizing t'  case app Γ _ σ τ _ _ _ _ _ =>    cases step    case appₗ | appᵣ => grind    case abs der _ _ =>      have sub : Sub Γ (σ.arrow τ) (σ.arrow τ) := by grind [Sub.refl]      have ⟨_, _, ⟨_, _⟩⟩ := der.abs_inv sub      grind [fresh_exists <| free_union [fvTm] Var, openTm_substTm_intro, subst_tm, Sub.weaken]  case tapp Γ _ σ τ σ' _ _ _ =>    cases step    case tabs der _ _ =>      have sub : Sub Γ (σ.all τ) (σ.all τ) := by grind [Sub.refl]      have ⟨_, _, ⟨_, _⟩⟩ := der.tabs_inv sub      have ⟨X, mem⟩ := fresh_exists <| free_union [Ty.fv, fvTy] Var      simp at mem      have : Γ = (Context.mapVal (·[X := σ']) []) ++ Γ := by grind      rw [openTy_substTy_intro (X := X), open_subst_intro (X := X)] <;> grind [subst_ty]    case tapp => grind  case let' Γ _ _ _ _ L der _ ih₁ _ =>    cases step    case let_bind red₁ _ => apply Typing.let' L (ih₁ red₁); grind    case let_body =>      grind [fresh_exists <| free_union [fvTm] Var, openTm_substTm_intro, subst_tm]  case case Γ _ σ τ _ _ _ L _ _ _ ih₁ _ _ =>    have sub : Sub Γ (σ.sum τ) (σ.sum τ) := by grind [Sub.refl]    have : Γ = [] ++ Γ := by rfl    cases step    case «case» red₁ _ _ => apply Typing.case L (ih₁ red₁) <;> grind    case case_inl der _ _ =>      have ⟨_, ⟨_, _⟩⟩ := der.inl_inv sub      grind [fresh_exists <| free_union [fvTm] Var, openTm_substTm_intro, subst_tm]    case case_inr der _ _ =>      have ⟨_, ⟨_, _⟩⟩ := der.inr_inv sub      grind [fresh_exists <| free_union [fvTm] Var, openTm_substTm_intro, subst_tm]  all_goals grind [cases Red]