∀ (parse : Std.Internal.Parsec.String.Parser Char) (size : ℕ) (_x : (_ : String) ×' ℕ),
  Std.Time.exactlyChars.go._unary✝ parse size _x =
    PSigma.casesOn _x fun acc count =>
      if count ≥ size then pure acc
      else do
        let res ← parse
        Std.Time.exactlyChars.go._unary✝¹ parse size ⟨acc.push res, count.succ⟩