Theorem: SCF.FOR_PEELING.CORRECT_r (MLIR/Dialects/ScfSemantics.lean)

State before:
n : ℕ
r : Region scf
args : TypedArgs scf
⊢ run (denoteRegion scf r args) (INPUT n) = Except.ok ([], INPUT n)
Tactic:
sorry
State after:
no goals