simp [set] at *
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H : set τ name v env = Except.ok (r, env')
name' : SSAVal
Hname : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧ set τ name v (SSAEnv.set name' τ' v' env) = Except.ok (r, env'')
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H :
  bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some val => raiseUB "setting to SSA value twice!"
        | none => StateT.set (SSAEnv.set name τ v s))
      env =
    Except.ok (r, env')
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      bind StateT.get
          (fun s =>
            match SSAEnv.get name τ s with
            | some val => raiseUB "setting to SSA value twice!"
            | none => StateT.set (SSAEnv.set name τ v s))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')