{α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LE α] →
      [DecidableLE α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLE α] →
            {n : Type u → Type w} →
              [Monad n] →
                (γ : Type u) →
                  (Pl : α → γ → ForInStep γ → Prop) →
                    (LargeEnough : α → Prop) →
                      (∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) →
                        (upperBound : α) →
                          γ →
                            (next : α) →
                              LargeEnough next →
                                ((out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (Pl out c))) →
                                  n γ