intros Hne env τ τ' val val' v₂ τ₂
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
⊢ v' ≠ v →
    ∀ ⦃env : SSAEnv δ⦄ ⦃τ τ' : MLIRType δ⦄ ⦃val : MLIRType.eval τ⦄ ⦃val' : MLIRType.eval τ'⦄,
      equiv (set v τ val (set v' τ' val' env)) (set v' τ' val' (set v τ val env))
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
v₂ : SSAVal
τ₂ : MLIRType δ
⊢ get v₂ τ₂ (set v τ val (set v' τ' val' env)) = get v₂ τ₂ (set v' τ' val' (set v τ val env))