Feature suggestion: foo.recommends for spec functions, similar to foo.requires for exec functions

[dschoepe]

recommends clauses provide a convenient way to express when the result of a spec function is meaningful. When proving theorems about such spec fns, it would be useful to refer to its recommends clause without repeating it. Similar functionality already exists for the requires clauses of exec functions. This can be worked around by moving the recommends clause into a separate spec fn and using it in both the recommends clause and the theorem about it, but this is less ergonomic. Would this be a useful feature to add?

(playground example)