simp[run_denoteRegion]
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteRegion scf
        (Region.mk "entry" []
          [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
        [])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
r₁ r₂ : Region scf
b : Bool
⊢ run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)