contradiction
case h_1
α₁ σ₁ : 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 Δ)
err✝ : String × SSAEnv Δ
heq✝ : denoteOp Δ head env = Except.error err✝
H : Except.error err✝ = 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