rw [H]
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
H :
  (match SSAEnv.get name τ env₂ with
    | some v => v
    | none => default) =
    r
a✝ : env₁ = env₁'
⊢ (match SSAEnv.get name τ env₂ with
    | some v => v
    | none => default) =
    r
no goals