simp[run_bind]
n : ℕ
r : Region scf
⊢ run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
                (AttrDict.mk [])])
      (INPUT n) =
    run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
              Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
                [r] (AttrDict.mk [])])
      (INPUT n)
n : ℕ
r : Region scf
⊢ (match run (denoteTypedArgs [] []) (INPUT n) with
    | Except.ok (a, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e) =
    match run (denoteTypedArgs [] []) (INPUT n) with
    | Except.ok (a, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
            Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e