Theorem: AlphaEquivPreservesType' (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
⊢ ∀ {M' 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' : σ)
Tactic:
intros M'
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M' : Λ V 𝕍
⊢ ∀ {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' : σ)

State before:
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 : σ)
Tactic:
introv
State after:
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 : σ)

State before:
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 : σ)
Tactic:
intros alpha_equiv ctxt_equiv
State after:
case Var
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
alpha_equiv : AlphaEquiv' var_map M (Λ.Var y)
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
⊢ (Γ ⊢ M : σ) → (Γ' ⊢ Λ.Var y : σ)

State before:
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 : AlphaEquiv' var_map (Λ.Var x) (Λ.Var y)
⊢ (Γ ⊢ Λ.Var x : σ) → (Γ' ⊢ Λ.Var y : σ)
Tactic:
simp at alpha_equiv
State after:
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 : σ)

State before:
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 : σ)
Tactic:
rcases alpha_equiv with var_map_x_to_y | ⟨var_map_x_is_none, x_eq_y⟩
State after:
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 : σ)

State before:
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 : σ)
Tactic:
specialize ctxt_equiv x
State after:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
var_map_x_to_y : var_map x = some y
ctxt_equiv : var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
⊢ (Γ ⊢ Λ.Var x : σ) → (Γ' ⊢ Λ.Var y : σ)

State before:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
var_map_x_to_y : var_map x = some y
ctxt_equiv : var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
⊢ (Γ ⊢ Λ.Var x : σ) → (Γ' ⊢ Λ.Var y : σ)
Tactic:
simp [var_map_x_to_y] at ctxt_equiv
State after:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
var_map_x_to_y : var_map x = some y
ctxt_equiv : getType x Γ = getType y Γ'
⊢ (Γ ⊢ Λ.Var x : σ) → (Γ' ⊢ Λ.Var y : σ)

State before:
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
var_map_x_to_y : var_map x = some y
ctxt_equiv : getType x Γ = getType y Γ'
⊢ (Γ ⊢ Λ.Var x : σ) → (Γ' ⊢ Λ.Var y : σ)
Tactic:
simp [ctxt_equiv]
State after:
no goals

State before:
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 : σ)
Tactic:
simp
State after:
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
⊢ getType x Γ = some σ → getType y Γ' = some σ

State before:
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
⊢ getType x Γ = some σ → getType y Γ' = some σ
Tactic:
specialize ctxt_equiv x
State after:
case inr.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
var_map_x_is_none : var_map x = none
x_eq_y : x = y
ctxt_equiv : var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
⊢ getType x Γ = some σ → getType y Γ' = some σ

State before:
case inr.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
var_map_x_is_none : var_map x = none
x_eq_y : x = y
ctxt_equiv : var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
⊢ getType x Γ = some σ → getType y Γ' = some σ
Tactic:
rw [←x_eq_y]
State after:
case inr.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
var_map_x_is_none : var_map x = none
x_eq_y : x = y
ctxt_equiv : var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
⊢ getType x Γ = some σ → getType x Γ' = some σ

State before:
case inr.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
var_map_x_is_none : var_map x = none
x_eq_y : x = y
ctxt_equiv : var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
⊢ getType x Γ = some σ → getType x Γ' = some σ
Tactic:
simp [var_map_x_is_none] at ctxt_equiv
State after:
case inr.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
var_map_x_is_none : var_map x = none
x_eq_y : x = y
ctxt_equiv : getType x Γ = getType x Γ'
⊢ getType x Γ = some σ → getType x Γ' = some σ

State before:
case inr.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
y : V
M : Λ V 𝕍
Γ Γ' : TCtxt V 𝕍
σ : 𝕋 𝕍
var_map : V → Option V
x : V
var_map_x_is_none : var_map x = none
x_eq_y : x = y
ctxt_equiv : getType x Γ = getType x Γ'
⊢ getType x Γ = some σ → getType x Γ' = some σ
Tactic:
simp [ctxt_equiv]
State after:
no goals

State before:
case App
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},
    AlphaEquiv' var_map M (Λ.App M₀' M₁') →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ Λ.App M₀' M₁' : σ)
Tactic:
introv
State after:
case App
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
⊢ AlphaEquiv' var_map M (Λ.App M₀' M₁') →
    (∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
      (Γ ⊢ M : σ) → (Γ' ⊢ Λ.App M₀' M₁' : σ)

State before:
case App
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
⊢ AlphaEquiv' var_map M (Λ.App M₀' M₁') →
    (∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
      (Γ ⊢ M : σ) → (Γ' ⊢ Λ.App M₀' M₁' : σ)
Tactic:
intros alpha_equiv ctxt_equiv h
State after:
case App
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
alpha_equiv : AlphaEquiv' var_map M (Λ.App M₀' M₁')
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
h : Γ ⊢ M : σ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ

State before:
case App
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
alpha_equiv : AlphaEquiv' var_map M (Λ.App M₀' M₁')
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
h : Γ ⊢ M : σ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ
Tactic:
match M with
| .App M₀ M₁ =>
  simp at alpha_equiv
  rw [←appl_rule] at h
  rcases h with ⟨τ, h₀, h₁⟩
  specialize ih₀ alpha_equiv.1 ctxt_equiv h₀
  specialize ih₁ alpha_equiv.2 ctxt_equiv h₁
  simp at ih₀ ih₁
  simp [ih₀, ih₁]
State after:
no goals

State before:
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 (Λ.App M₀ M₁) (Λ.App M₀' M₁')
h : Γ ⊢ Λ.App M₀ M₁ : σ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ
Tactic:
simp at alpha_equiv
State after:
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 : Γ ⊢ Λ.App M₀ M₁ : σ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ

State before:
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 : Γ ⊢ Λ.App M₀ M₁ : σ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ
Tactic:
rw [←appl_rule] at h
State after:
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 : ∃ σ_1, (Γ ⊢ M₀ : σ_1 →' σ) ∧ (Γ ⊢ M₁ : σ_1)
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ

State before:
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 : ∃ σ_1, (Γ ⊢ M₀ : σ_1 →' σ) ∧ (Γ ⊢ M₁ : σ_1)
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ
Tactic:
rcases h with ⟨τ, h₀, h₁⟩
State after:
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₁' : σ

State before:
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₁' : σ
Tactic:
specialize ih₀ alpha_equiv.1 ctxt_equiv h₀
State after:
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₁' : σ

State before:
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₁' : σ
Tactic:
specialize ih₁ alpha_equiv.2 ctxt_equiv h₁
State after:
case intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
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₀' : τ →' σ
ih₁ : Γ' ⊢ M₁' : τ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ

State before:
case intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
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₀' : τ →' σ
ih₁ : Γ' ⊢ M₁' : τ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ
Tactic:
simp at ih₀ ih₁
State after:
case intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
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₀ : typeOf Γ' M₀' = some (τ →' σ)
ih₁ : typeOf Γ' M₁' = some τ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ

State before:
case intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
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₀ : typeOf Γ' M₀' = some (τ →' σ)
ih₁ : typeOf Γ' M₁' = some τ
⊢ Γ' ⊢ Λ.App M₀' M₁' : σ
Tactic:
simp [ih₀, ih₁]
State after:
no goals

State before:
case Lam
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},
    AlphaEquiv' var_map M (λ' x' : τ', M') →
      (∀ (x : V),
          var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
        (Γ ⊢ M : σ) → (Γ' ⊢ λ' x' : τ', M' : σ)
Tactic:
introv
State after:
case Lam
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
⊢ AlphaEquiv' var_map M (λ' x' : τ', M') →
    (∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
      (Γ ⊢ M : σ) → (Γ' ⊢ λ' x' : τ', M' : σ)

State before:
case Lam
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
⊢ AlphaEquiv' var_map M (λ' x' : τ', M') →
    (∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ') →
      (Γ ⊢ M : σ) → (Γ' ⊢ λ' x' : τ', M' : σ)
Tactic:
intros alpha_equiv ctxt_equiv h
State after:
case Lam
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
alpha_equiv : AlphaEquiv' var_map M (λ' x' : τ', M')
ctxt_equiv :
  ∀ (x : V), var_map x = none ∧ getType x Γ = getType x Γ' ∨ ∃ y, var_map x = some y ∧ getType x Γ = getType y Γ'
h : Γ ⊢ M : σ
⊢ Γ' ⊢ λ' x' : τ', M' : σ

State before:
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' var_map (λ' x : τ, M) (λ' x' : τ', M')
h : Γ ⊢ λ' x : τ, M : σ
⊢ Γ' ⊢ λ' x' : τ', M' : σ
Tactic:
simp at alpha_equiv
State after:
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' ∧ τ = τ'
h : Γ ⊢ λ' x : τ, M : σ
⊢ Γ' ⊢ λ' x' : τ', M' : σ

State before:
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' ∧ τ = τ'
h : Γ ⊢ λ' x : τ, M : σ
⊢ Γ' ⊢ λ' x' : τ', M' : σ
Tactic:
simp at h
State after:
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' ∧ τ = τ'
h :
  (match typeOf (Γ;; x : τ) M with
    | some τ_1 => some (τ →' τ_1)
    | x => none) =
    some σ
⊢ Γ' ⊢ λ' x' : τ', M' : σ

State before:
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' ∧ τ = τ'
h :
  (match typeOf (Γ;; x : τ) M with
    | some τ_1 => some (τ →' τ_1)
    | x => none) =
    some σ
⊢ Γ' ⊢ λ' x' : τ', M' : σ
Tactic:
generalize h' : typeOf (Γ;; x : τ) M = aux
State after:
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' ∧ τ = τ'
h :
  (match typeOf (Γ;; x : τ) M with
    | some τ_1 => some (τ →' τ_1)
    | x => none) =
    some σ
aux : Option (𝕋 𝕍)
h' : typeOf (Γ;; x : τ) M = aux
⊢ Γ' ⊢ λ' x' : τ', M' : σ

State before:
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' ∧ τ = τ'
h :
  (match typeOf (Γ;; x : τ) M with
    | some τ_1 => some (τ →' τ_1)
    | x => none) =
    some σ
aux : Option (𝕋 𝕍)
h' : typeOf (Γ;; x : τ) M = aux
⊢ Γ' ⊢ λ' x' : τ', M' : σ
Tactic:
rw [h'] at h
State after:
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 :
  (match aux with
    | some τ_1 => some (τ →' τ_1)
    | x => none) =
    some σ
h' : typeOf (Γ;; x : τ) M = aux
⊢ Γ' ⊢ λ' x' : τ', M' : σ

State before:
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 :
  (match some σ' with
    | some τ_1 => some (τ →' τ_1)
    | x => none) =
    some σ
h' : typeOf (Γ;; x : τ) M = some σ'
⊢ Γ' ⊢ λ' x' : τ', M' : σ
Tactic:
simp at h
State after:
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 : (τ →' σ') = σ
⊢ Γ' ⊢ λ' x' : τ', M' : σ

State before:
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 : (τ →' σ') = σ
⊢ Γ' ⊢ λ' x' : τ', M' : σ
Tactic:
rw [alpha_equiv.2] at h
State after:
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 : (τ' →' σ') = σ
⊢ Γ' ⊢ λ' x' : τ', M' : σ

State before:
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 : (τ' →' σ') = σ
⊢ Γ' ⊢ λ' x' : τ', M' : σ
Tactic:
rw [←h]
State after:
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 : (τ' →' σ') = σ
⊢ Γ' ⊢ λ' x' : τ', M' : τ' →' σ'

State before:
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 : (τ' →' σ') = σ
⊢ Γ' ⊢ λ' x' : τ', M' : τ' →' σ'
Tactic:
simp
State after:
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 : (τ' →' σ') = σ
⊢ (match typeOf (Γ';; x' : τ') M' with
    | some τ => some (τ' →' τ)
    | x => none) =
    some (τ' →' σ')

State before:
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 (τ' →' σ')
Tactic:
specialize ih alpha_equiv.1 ctxt_equiv' h'
State after:
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 (τ' →' σ')

State before:
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 (τ' →' σ')
Tactic:
rw [ih]
State after:
no goals

State before:
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 : (τ' →' σ') = σ
⊢ ∀ (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' : τ')
Tactic:
introv
State after:
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 : (τ' →' σ') = σ
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' : τ')

State before:
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 : (τ' →' σ') = σ
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' : τ')
Tactic:
by_cases h : y = x
State after:
case pos
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✝ : (τ' →' σ') = σ
y : V
h : y = x
⊢ (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' : τ')

case neg
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✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
⊢ (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' : τ')

State before:
case pos
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✝ : (τ' →' σ') = σ
y : V
h : y = x
⊢ (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' : τ')
Tactic:
simp [h, alpha_equiv.2]
State after:
no goals

State before:
case neg
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✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
⊢ (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' : τ')
Tactic:
simp [h]
State after:
case neg
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✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
⊢ (var_map y = none ∧ getType y Γ = if y = x' then some τ' else getType y Γ') ∨
    ∃ z, var_map y = some z ∧ getType y Γ = if z = x' then some τ' else getType z Γ'

State before:
case neg
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✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
⊢ (var_map y = none ∧ getType y Γ = if y = x' then some τ' else getType y Γ') ∨
    ∃ z, var_map y = some z ∧ getType y Γ = if z = x' then some τ' else getType z Γ'
Tactic:
specialize ctxt_equiv y
State after:
case neg
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
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✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
ctxt_equiv : var_map y = none ∧ getType y Γ = getType y Γ' ∨ ∃ y_1, var_map y = some y_1 ∧ getType y Γ = getType y_1 Γ'
⊢ (var_map y = none ∧ getType y Γ = if y = x' then some τ' else getType y Γ') ∨
    ∃ z, var_map y = some z ∧ getType y Γ = if z = x' then some τ' else getType z Γ'

State before:
case neg
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
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✝ : (τ' →' σ') = σ
y : V
h : ¬y = x
ctxt_equiv : var_map y = none ∧ getType y Γ = getType y Γ' ∨ ∃ y_1, var_map y = some y_1 ∧ getType y Γ = getType y_1 Γ'
⊢ (var_map y = none ∧ getType y Γ = if y = x' then some τ' else getType y Γ') ∨
    ∃ z, var_map y = some z ∧ getType y Γ = if z = x' then some τ' else getType z Γ'
Tactic:
sorry
State after:
no goals