Description
All relations are now parameterized by a relation L on labels, encompassing hence at once the itree-style relational postcondition passed to eutt, as well as the generalization rutt allowing to map distinct events one to another.
Currently, the type label reflects through a type parameter the signature of computations it applies to, but not its return type. It was coined this way to avoid awkward type transports when considering transitions in bind constructions, but has the drawbacks of making the relational specification L awkward: it is not aware of the return type specifically.
Additionally, having all baked into a single relation is sometimes weird: while the relation on val labels certainly must change when running a cut rule, the part on obs and tau must be invariant.
TODO: revisit these tradeoff. Expose the return type in the type of labels? Explicitly break relations into a val relation and an event relation?