∀ {α : Type u} {n : Type u → Type u_1} [inst : Std.PRange.UpwardEnumerable α]
  [inst_1 : Std.PRange.LawfulUpwardEnumerable α] [inst_2 : Monad n] [LawfulMonad n] {γ : Type u}
  {LargeEnough : α → Prop} {hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b}
  {next : α} {hn : LargeEnough next} {acc : γ} (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxi.Iterator α) Id Pl)
  (f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (Pl out c))),
  Std.Rxi.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl acc next hn f =
    Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc next hn f