intros env₁ env₂ Hequiv τ name r env₁'
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃env₁ env₂ : SSAEnv Δ⦄,
    SSAEnv.equiv env₁ env₂ →
      ∀ ⦃τ : MLIRType Δ⦄ ⦃name : SSAVal⦄ ⦃r : MLIRType.eval τ⦄ ⦃env₁' : SSAEnv Δ⦄,
        get τ name 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 Δ
⊢ get τ name env₁ = Except.ok (r, env₁') → get τ name env₂ = Except.ok (r, env₂)