Theorem: AlphaEquivPreservesType (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
⊢ ∀ {M M' : Λ V 𝕍} {Γ : TCtxt V 𝕍} {σ : 𝕋 𝕍}, (M =ₐ M') → (Γ ⊢ M : σ) → (Γ ⊢ M' : σ)
Tactic:
introv
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
⊢ (M =ₐ M') → (Γ ⊢ M : σ) → (Γ ⊢ M' : σ)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
⊢ (M =ₐ M') → (Γ ⊢ M : σ) → (Γ ⊢ M' : σ)
Tactic:
intro h h'
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
⊢ Γ ⊢ M' : σ

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
⊢ Γ ⊢ M' : σ
Tactic:
exact AlphaEquivPreservesType' h (by introv; simp) h'
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
⊢ ∀ (x : V), none = none ∧ getType x Γ = getType x Γ ∨ ∃ y, none = some y ∧ getType x Γ = getType y Γ
Tactic:
introv
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
x : V
⊢ none = none ∧ getType x Γ = getType x Γ ∨ ∃ y, none = some y ∧ getType x Γ = getType y Γ

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
M M' : Λ V 𝕍
Γ : TCtxt V 𝕍
σ : 𝕋 𝕍
h : M =ₐ M'
h' : Γ ⊢ M : σ
x : V
⊢ none = none ∧ getType x Γ = getType x Γ ∨ ∃ y, none = some y ∧ getType x Γ = getType y Γ
Tactic:
simp
State after:
no goals