Here's something else you can do.
OpAction(a) == ...
...
Next == \/ \E a \in ... : MessageAction(OpAction(a), ...) \/ ...
Leslie