Describe the termination behaviour in seq.mli

[hirrolot]

As suggested by @dbuenzli in this comment, seq.mli is "littered" with statements like "The sequence [xs] must be finite.". However, most of these preconditions are too strict, in the sense that many Seq functions, such as for_all/exists or find/find_index/find_map/etc., may terminate even on infinite sequences.

This PR touches only the documentation of the Seq functions.

Initially, I planned to make this change after my PR #13750 is merged, but since it got delayed due to a second approval, I assume it's better to improve the documentation now than later.

On phrasing

Two sentences were suggested (mind the order):

1. Guaranteed to terminate only if [xs] is finite.
2. May not terminate if [xs] is infinite.

When expanded, these phrases mean:

1. Guaranteed to terminate if [xs] is finite, but may or may not terminate if [xs] is infinite.
2. May or may not terminate if [xs] is infinite, and the same for when [xs] is finite.

Clearly, the first one is formally more correct. But since it seems pretty clear that sequence-consuming functions always terminate on finite xs/ys, I decided to use the more concise phrasing.

[gasche]

This now looks good to me.

[gasche]

Thanks! Merged.