intros env₁ env₂ Hequiv τ name v r env₁'
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃env₁ env₂ : SSAEnv Δ⦄,
    SSAEnv.equiv env₁ env₂ →
      ∀ ⦃τ : MLIRType Δ⦄ ⦃name : SSAVal⦄ ⦃v : MLIRType.eval τ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
        set τ name v env₁ = Except.ok (r, env₁') → set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ set τ name v env₁ = Except.ok (r, env₁') → set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)