simp at Hv
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝¹ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
x✝ : Option (MLIRType.eval argsHead.fst)
heq✝ : SSAEnv.get headVal argsHead.fst env = none
Hv : Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok (PUnit.unit, snd)
⊢ Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) =
      Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
argsHead : TypedArg δ
argsTail : TypedArgs δ
env : SSAEnv δ
res : Unit
env' : SSAEnv δ
headVal : SSAVal
tailVal : List SSAVal
x✝¹ : Except (String × SSAEnv δ) (Unit × SSAEnv δ)
v : Unit × SSAEnv δ
snd : SSAEnv δ
H : denoteTypedArgs argsTail tailVal snd = Except.ok (res, env')
x✝ : Option (MLIRType.eval argsHead.fst)
heq✝ : SSAEnv.get headVal argsHead.fst env = none
Hv : SSAEnv.set headVal argsHead.fst argsHead.snd env = snd
⊢ Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) =
      Except.ok ((), SSAEnv.set headVal argsHead.fst argsHead.snd env) ∧
    denoteTypedArgs argsTail tailVal (SSAEnv.set headVal argsHead.fst argsHead.snd env) = Except.ok ((), env')