case nil =>
  intros env r resEnv H
  simp [denoteOpArgs] at *
  simp_monad at *
  cases H; subst r env; simp
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ [] env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all [] fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ [] (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
no goals