simp[run_denoteOps_singleton]
n : ℕ
r : Region scf
⊢ run
      (denoteOps scf
        [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n) =
    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 [])])
      (INPUT n)
n : ℕ
r : Region scf
⊢ run
      (denoteOp scf
        (Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
          (AttrDict.mk [])))
      (INPUT n) =
    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 [])])
      (INPUT n)