rw [SSAScope.getT_set_ne]
case One
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ SSAScope.getT v (SSAScope.set v' τ val s) = SSAScope.getT v s
case One.a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ v' ≠ v