∀ (bs : ByteArray) (_x : (_ : ℕ) ×' List UInt8),
  ByteArray.toList.loop._unary bs _x =
    PSigma.casesOn _x fun i r =>
      if i < bs.size then ByteArray.toList.loop._unary bs ⟨i + 1, bs.get! i :: r⟩ else r.reverse