rcases alpha_equiv with var_map_x_to_y | ⟨var_map_x_is_none, x_eq_y⟩
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
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
alpha_equiv : var_map x = some y ∨ var_map x = none ∧ x = y
⊢ (Γ ⊢ Λ.Var x : σ) → (Γ' ⊢ Λ.Var y : σ)
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
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
var_map_x_to_y : var_map x = some y
⊢ (Γ ⊢ Λ.Var x : σ) → (Γ' ⊢ Λ.Var y : σ)

case inr.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
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
var_map_x_is_none : var_map x = none
x_eq_y : x = y
⊢ (Γ ⊢ Λ.Var x : σ) → (Γ' ⊢ Λ.Var y : σ)