rw [TopM.set_unfold]
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₁ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, env₁') →
    set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₁ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, env₁') →
    (match SSAEnv.get name τ env₂ with
      | some val => Except.error ("setting to SSA value twice!", env₂)
      | none => Except.ok ((), SSAEnv.set name τ v env₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)