specialize ih alpha_equiv.1 ctxt_equiv' h'
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
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 Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h : (τ' →' σ') = σ
ctxt_equiv' :
  ∀ (y : V),
    (if y = x then some x' else var_map y) = none ∧ getType y (Γ;; x : τ) = getType y (Γ';; x' : τ') ∨
      ∃ z, (if y = x then some x' else var_map y) = some z ∧ getType y (Γ;; x : τ) = getType z (Γ';; x' : τ')
⊢ (match typeOf (Γ';; x' : τ') M' with
    | some τ => some (τ' →' τ)
    | x => none) =
    some (τ' →' σ')
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x' : V
τ' : 𝕋 𝕍
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 Γ'
x : V
τ : 𝕋 𝕍
M : Λ V 𝕍
alpha_equiv : AlphaEquiv' (fun vn => if vn = x then some x' else var_map vn) M M' ∧ τ = τ'
aux : Option (𝕋 𝕍)
σ' : 𝕋 𝕍
h' : typeOf (Γ;; x : τ) M = some σ'
h : (τ' →' σ') = σ
ctxt_equiv' :
  ∀ (y : V),
    (if y = x then some x' else var_map y) = none ∧ getType y (Γ;; x : τ) = getType y (Γ';; x' : τ') ∨
      ∃ z, (if y = x then some x' else var_map y) = some z ∧ getType y (Γ;; x : τ) = getType z (Γ';; x' : τ')
ih : (Γ';; x' : τ') ⊢ M' : σ'
⊢ (match typeOf (Γ';; x' : τ') M' with
    | some τ => some (τ' →' τ)
    | x => none) =
    some (τ' →' σ')