case cons head tail HInd =>
  intros env₂ Henv₂
  simp [denoteOpArgs]; simp [denoteOpArgs] at H
  have ⟨headName, headτ⟩ := head
  simp_monad at *
  revert H
  cases Hhead: TopM.get headτ headName env <;> simp <;> intros H <;> try contradiction
  case ok headR =>
  have ⟨headR, headEnv⟩ := headR
  simp [TopM.get_equiv Henv₂ Hhead]
  split at H <;> try contradiction
  case h_2 tailR HTailR =>
  simp at H; cases H; subst env' r
  have ⟨tailR, tailEnv⟩ := tailR; simp at HTailR
  have AOEU := HInd HTailR
  rw [TopM.get_unfold] at Hhead; simp at Hhead; cases Hhead; subst env
  specialize HInd HTailR Henv₂
  simp [denoteOpArgs] at HInd
  simp_monad at *
  simp [HInd]
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ (head :: tail) env₂ = Except.ok (r, env₂)
no goals