case h_2 headR HHeadR =>
have ⟨headR, headEnv⟩ := headR; simp at *
have ⟨envHead, HenvHead, HdenoteHead⟩ := denoteOp_equiv HHeadR Henv₂
simp [HdenoteHead]
rw [←TAIL] at H; rw [←TAIL]
apply denoteOps_equiv H HenvHead
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
head : Op Δ
tail : List (Op Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
head2 : Op Δ
tail2 : List (Op Δ)
TAIL : tail = head2 :: tail2
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
headR : List (TypedArg Δ) × SSAEnv Δ
HHeadR : denoteOp Δ head env = Except.ok headR
H : denoteOps Δ (head2 :: tail2) headR.snd = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOp Δ head env₂ with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ (head2 :: tail2) v.snd) =
        Except.ok (res, env₂')
no goals