cases HregIn
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HregIn : region = TopM.scoped ∘ denoteRegion Δ head ∨ region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
case inl
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
h✝ : region = TopM.scoped ∘ denoteRegion Δ head
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')

case inr
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
h✝ : region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')