rw [denoteTypedArgs_cons_unfold]
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (PUnit.unit, env₂')
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    bind (TopM.set argsHead.fst valsHead argsHead.snd) (fun x => denoteTypedArgs argsTail valsTail) env₂ =
      Except.ok (PUnit.unit, env₂')