have HHead₂ := TopM.set_equiv Henv₂ HHead
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
env₁ : SSAEnv Δ
r : Unit
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₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
env₁ : SSAEnv Δ
r : Unit
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₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')