Changing basic definitions in Prosa
Currently, prosa definitions do not leverage other definitions enough. This often leads to unnecessarily longer and harder proofs. We should use already existing definitions wherever possible. In particular, defining new big_ops should be avoided as much as possible by building on top of old bigops.
For example, task_served_at
is defined using receives_service_at
but not using served_jobs_at
We can use this issue to collect other instances of sub-optimal definitions.