simp [TopM.set]
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ set τ name v 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)
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ 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 =
    match SSAEnv.get name τ env with
    | some val => Except.error ("setting to SSA value twice!", env)
    | none => Except.ok ((), SSAEnv.set name τ v env)