exists (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) env'' ∧
      (match SSAEnv.get name τ env with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)) ∧
    (match SSAEnv.get name τ env with
        | some val => raiseUB "setting to SSA value twice!"
        | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
        (SSAEnv.set name' τ' v' env) =
      Except.ok (r, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))