rw [H]
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
H : (PUnit.unit, SSAEnv.set name τ v env) = r
⊢ r = ((), SSAEnv.set name τ v env)
no goals