simp [h']
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
no goals