intros τ name env r env' H name' Hne τ' v'
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃τ : MLIRType Δ⦄ ⦃name : SSAVal⦄ ⦃env : SSAEnv Δ⦄ ⦃r : MLIRType.eval τ⦄ ⦃env' : SSAEnv Δ⦄,
    get τ name env = Except.ok (r, env') →
      ∀ ⦃name' : SSAVal⦄,
        name' ≠ name →
          ∀ ⦃τ' : MLIRType Δ⦄ ⦃v' : MLIRType.eval τ'⦄,
            get τ name (SSAEnv.set name' τ' v' env) = Except.ok (r, SSAEnv.set name' τ' v' env')
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
H : get τ name env = Except.ok (r, env')
name' : SSAVal
Hne : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ get τ name (SSAEnv.set name' τ' v' env) = Except.ok (r, SSAEnv.set name' τ' v' env')