simp_monad at *
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
H :
  Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env) =
    Except.ok (r, env')
name' : SSAVal
Hne : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ Except.ok
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
        | some v => v
        | none => default,
        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 Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
H :
  (match SSAEnv.get name τ env with
      | some v => v
      | none => default) =
      r ∧
    env = env'
⊢ (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
      | some v => v
      | none => default) =
      r ∧
    SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'