introv
case Var
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
⊢ ∀ {M : Λ V 𝕍} {Γ Γ' : TCtxt V 𝕍} {σ : 𝕋 𝕍} {var_map : V → Option V},
    AlphaEquiv' var_map M (Λ.Var y) →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ Λ.Var y : σ)
case Var
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
⊢ AlphaEquiv' var_map M (Λ.Var y) →
    (∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
      (Γ ⊢ M : σ) → (Γ' ⊢ Λ.Var y : σ)