case cons head tail HInd =>
  intros env r resEnv H name Hname τ v
  simp [denoteOpArgs]; simp [denoteOpArgs] at H
  have ⟨headName, headτ⟩ := head
  simp_monad at *
  cases Hhead: (TopM.get headτ headName env)
  case error _ =>
    rw [Hhead] at H; contradiction
  case ok headRes =>
    rw [Hhead] at H
    simp [List.all, List.foldr] at Hname
    have ⟨Hname_head, _⟩ := Hname
    rw [TopM.get_env_set_commutes Hhead Hname_head]
    simp at *
    split at H <;> try contradiction
    case h_2 rTail Htail =>
    have ⟨rTailRes, rTailEnv⟩ := rTail
    simp at H; have ⟨_, _⟩ := H; subst r resEnv
    simp [denoteOpArgs] at *
    simp [bind, StateT.bind, Except.bind, pure, StateT.pure, Except.pure] at HInd
    rw [HInd] <;> assumption
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ (head :: tail) env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ (head :: tail) (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
no goals