simp_monad
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ 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 →
    r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ (match SSAEnv.get name τ env with
        | some val => raiseUB "setting to SSA value twice!"
        | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
        env =
      Except.ok r →
    r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none