simp[run_denoteTypedArgs_nil]
r₁ r₂ : Region scf
b : Bool
⊢ (match run (denoteTypedArgs [] []) (INPUT b) with
    | Except.ok (PUnit.unit, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
r₁ r₂ : Region scf
b : Bool
⊢ run
      (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)