split_ifs <;> rfl
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 Γ
no goals