Wf lemma

@[grind →]lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : Γ.Wf ∧ t.LC ∧ τ.Wf Γ := by  induction der <;> let L := free_union Var <;> have ⟨x, nmem⟩ := fresh_exists L  case tabs ih =>    cases (ih x (by grind)).left    split_ands    · grind    · apply LC.tabs L <;> grind    · apply Ty.Wf.all L <;> grind  case abs ih =>    cases (ih x (by grind)).left    grind [LC.abs L, Wf.strengthen]  case let' => grind [LC.let' L, Ty.Wf.strengthen]  case case => refine ⟨?_, LC.case L ?_ ?_ ?_, ?_⟩ <;> grind [Ty.Wf.strengthen]  case var => grind [of_bind_ty]  case app => grind only [LC.app, cases Ty.Wf]  all_goals grind [open_lc]