rw [HdenoteArgs]
case h_2.unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps (PUnit.unit, argsEnv).snd = Except.ok (res, env')
argsEnv₂ : SSAEnv Δ
HargsEnv₂ : SSAEnv.equiv argsEnv argsEnv₂
HdenoteArgs : denoteTypedArgs args (List.map Prod.fst rArgs) env₂ = Except.ok (PUnit.unit, argsEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteTypedArgs args (List.map Prod.fst rArgs) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')
case h_2.unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
argsR : Unit × SSAEnv Δ
argsEnv : SSAEnv Δ
HargsR : denoteTypedArgs args (List.map Prod.fst rArgs) env = Except.ok (PUnit.unit, argsEnv)
H : denoteOps Δ rOps (PUnit.unit, argsEnv).snd = Except.ok (res, env')
argsEnv₂ : SSAEnv Δ
HargsEnv₂ : SSAEnv.equiv argsEnv argsEnv₂
HdenoteArgs : denoteTypedArgs args (List.map Prod.fst rArgs) env₂ = Except.ok (PUnit.unit, argsEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match Except.ok (PUnit.unit, argsEnv₂) with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ rOps v.snd) =
        Except.ok (res, env₂')