match TAIL: tail with
| .nil =>
  apply denoteOp_equiv <;> assumption
| .cons head2 tail2 =>
  simp [denoteOps] at *; simp_monad at *
  split at H <;> try contradiction
  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₂
H :
  (match head :: tail with
      | [] => fun s => Except.ok ([], s)
      | [stmt] => denoteOp Δ stmt
      | stmt :: stmts' => fun s =>
        match denoteOp Δ stmt s with
        | Except.error err => Except.error err
        | Except.ok v => denoteOps Δ stmts' v.snd)
      env =
    Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ (head :: tail) env₂ = Except.ok (res, env₂')
no goals