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