specialize (HInd Hrun Henv₂)
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
HInd :
  ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
HInd : ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx' args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')