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