∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  {n : Type u → Type w} [inst_2 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (acc : γ) (next : α)
  (h : LargeEnough next) (f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (Pl out c))),
  Std.Rxi.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl acc next h f =
    WellFounded.extrinsicFix₃
      (InvImage (Std.IteratorLoop.rel (Std.Rxi.Iterator α) Id Pl) fun x =>
        ({ internalState := { next := some x.fst } }, x.snd.fst))
      (fun next acc h G => do
        let __do_lift ← f next h acc
        match __do_lift with
          | ⟨ForInStep.yield acc', h'⟩ =>
            match hs : Std.PRange.succ? next with
            | some next' => G next' acc' ⋯ ⋯
            | none => pure acc'
          | ⟨ForInStep.done acc', property⟩ => pure acc')
      next acc h