induction M with
| Var x => intro Γ Γ' h; apply h; simp
| App M N ih₁ ih₂ =>
  intro Γ Γ' h
  have h₁ (x : V) (h' : x ∈ freeVarsOfTerm M) : getType x Γ = getType x Γ' := by
    exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', true_or])
  have h₂ (x : V) (h' : x ∈ freeVarsOfTerm N) : getType x Γ = getType x Γ' := by
    exact h x (by simp only [freeVarsOfTerm, Finset.mem_union, h', or_true])
  simp [ih₁ h₁, ih₂ h₂]
| Lam y σ M ih => 
  intro Γ Γ' h
  have h (x : V) (h' : x ∈ freeVarsOfTerm M) : getType x (Γ;; y : σ) = getType x (Γ';; y : σ) := by
    by_cases h'' : x = y <;> simp[h'']
    exact h x (Finset.mem_erase_of_ne_of_mem h'' h')
  simp [ih h]
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M : Λ V 𝕍
⊢ ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
no goals