rw [TopM.get_unfold]
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₁ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    get τ name env₂ = Except.ok (r, env₂)
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₁ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₂) =
      Except.ok (r, env₂)