simp [TopM.get]
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ get τ name env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some v => pure v
        | none => pure default)
      env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)