∀ (pred : UInt8 → Bool) (limit : ℕ) (_x : (_ : ℕ) ×' ByteArray.Iterator),
  Std.Internal.Parsec.ByteArray.takeWhileUpTo1.findEnd._unary✝ pred limit _x =
    PSigma.casesOn _x fun count iter =>
      if count ≥ limit then (count, iter)
      else
        if ¬iter.hasNext = true then (count, iter)
        else
          if pred iter.curr = true then
            Std.Internal.Parsec.ByteArray.takeWhileUpTo1.findEnd._unary✝¹ pred limit ⟨count + 1, iter.next⟩
          else (count, iter)