induction args
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
args : TypedArgs Δ
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs args vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs args vals env₂ = Except.ok (r, env₂')
case nil
α₁ σ₁ : 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₂')

case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head✝ : TypedArg Δ
tail✝ : List (TypedArg Δ)
tail_ih✝ :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs tail✝ vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs tail✝ vals env₂ = Except.ok (r, env₂')
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs (head✝ :: tail✝) vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (head✝ :: tail✝) vals env₂ = Except.ok (r, env₂')