rw[OpM_toTopM_denoteRegion]
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₂ 1 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)
r₁ r₂ : Region scf
⊢ run (TopM.denoteRegionsByIx [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] 1 [])
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)