. rw [get_set_ne_val]
  assumption
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : ¬v' = v
⊢ get v τ (set v' τ' val env) = get v τ env
no goals