Theorem: getTypeRebind (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
⊢ ∀ (x : V), getType x ((Γ;; y : σ);; y : σ') = getType x (Γ;; y : σ')
Tactic:
introv
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
x : V
⊢ getType x ((Γ;; y : σ);; y : σ') = getType x (Γ;; y : σ')

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
x : V
⊢ getType x ((Γ;; y : σ);; y : σ') = getType x (Γ;; y : σ')
Tactic:
simp
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
x : V
⊢ (if x = y then some σ' else if x = y then some σ else getType x Γ) = if x = y then some σ' else getType x Γ

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
y : V
σ σ' : 𝕋 𝕍
x : V
⊢ (if x = y then some σ' else if x = y then some σ else getType x Γ) = if x = y then some σ' else getType x Γ
Tactic:
split_ifs <;> rfl
State after:
no goals