simp[INPUT]
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match run (TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b")) (INPUT b) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (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
⊢ (match
      match
        run (TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b"))
          (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    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)