simp[OpM.denoteRegions]
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (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)
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            [OpM.denoteRegion r₁ 0, OpM.denoteRegion r₂ 1] (AttrDict.mk []))))
      (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)