contradiction
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
H : denoteRegionsEquivInvariant []
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx [] idx args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx [] idx args env₂ = Except.ok (res, env₂')
no goals