specialize ih₀ alpha_equiv.1 ctxt_equiv h₀
case intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M₀' M₁' : Λ V 𝕍
ih₀ :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M₀' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M₀' : σ)
ih₁ :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M₁' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M₁' : σ)
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
M₀ M₁ : Λ V 𝕍
alpha_equiv : AlphaEquiv' var_map M₀ M₀' ∧ AlphaEquiv' var_map M₁ M₁'
τ : 𝕋 𝕍
h₀ : Γ ⊢ M₀ : τ →' σ
h₁ : Γ ⊢ M₁ : τ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ
case intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M₀' M₁' : Λ V 𝕍
ih₁ :
  ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M M₁' →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ M₁' : σ)
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
M₀ M₁ : Λ V 𝕍
alpha_equiv : AlphaEquiv' var_map M₀ M₀' ∧ AlphaEquiv' var_map M₁ M₁'
τ : 𝕋 𝕍
h₀ : Γ ⊢ M₀ : τ →' σ
h₁ : Γ ⊢ M₁ : τ
ih₀ : Γ' ⊢ M₀' : τ →' σ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ