apply denoteOp_equiv <;> assumption
α₁ σ₁ : 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] 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')
TAIL : tail = []
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ denoteOps Δ [head] env₂ = Except.ok (res, env₂')
no goals