case nil =>
  intros val env₁ r env₁' H env₂ Henv₂
  simp [denoteTypedArgs] at *
  exists env₂
  simp_monad at *; subst H; assumption
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs [] vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ → ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs [] vals env₂ = Except.ok (r, env₂')
no goals