Return pattern for STS's

There's a pattern that happens sometimes, where the state `S` of an STS is of the form `S' × R`, and we only care about stepping from `(s', 0)` (for some reasonable definition of `0`) to `(s'', r)`, where `r` is then used for other stuff but not used in future invocations of that STS. It may be worth thinking about some custom syntax & other goodies for this pattern.