∀ (x : ℕ) (s : String) (b e : String.Pos.Raw),
  { str := s, startPos := b, stopPos := e }.take x =
    { str := s, startPos := b, stopPos := ({ str := s, startPos := b, stopPos := e }.nextn x 0).offsetBy b }