simp only [freeVarsOfTerm, Finset.mem_union, h', or_true]
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M N : Λ V 𝕍
ih₁ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ') → typeOf Γ M = typeOf Γ' M
ih₂ : ∀ {Γ Γ' : TCtxt V 𝕍}, (∀ (x : V), x ∈ freeVarsOfTerm N → getType x Γ = getType x Γ') → typeOf Γ N = typeOf Γ' N
Γ Γ' : TCtxt V 𝕍
h : ∀ (x : V), x ∈ freeVarsOfTerm (Λ.App M N) → getType x Γ = getType x Γ'
h₁ : ∀ (x : V), x ∈ freeVarsOfTerm M → getType x Γ = getType x Γ'
x : V
h' : x ∈ freeVarsOfTerm N
⊢ x ∈ freeVarsOfTerm (Λ.App M N)
no goals