Extend Lin and STM to support multiple tested `t`s

[jmid]

Both Lin and STM share a limitation:

• Lin tests only a single t at a time
• STM tests only a single sut at a time

This can be worked around, e.g., by using a list of suts in STM - but it is a bit of a hack. Furthermore, it is quite common to have multiple values of a mutable type, e.g., arising from Array.copy or Buffer.of_seq. It would be nice to address this limitation.