simp
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂'_1,
    SSAEnv.equiv env' env₂'_1 ∧
      (match Except.ok (resReg, env₂') with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂'_1)
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)