simp [refines, SSAEnv.refines]
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
⊢ refines env1 env2 → refines (set name τ val env1) (set name τ val env2)
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
⊢ (∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
      getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }) →
    ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
      getT v (set name τ val env2) = some { fst := a, snd := b } →
        getT v (set name τ val env1) = some { fst := a, snd := b }