cases b <;> simp
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (ite (b = false → False) (OpM.denoteRegion r₁ 0) (OpM.denoteRegion r₂ 1) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
case false
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)

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