cases env with
| One s =>
  simp [getT, set]
  rw [SSAScope.getT_set_ne]
  assumption
| Cons head tail =>
  simp [getT, set, HOrElse.hOrElse, OrElse.orElse, Option.orElse]
  rw [SSAScope.getT_set_ne]
  assumption
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v' τ val env) = getT v env
no goals