These are macros of the Pluscal language aren't they. (3.5 p. 28)
In fact I meant a predicate expressed as a TLA+ operator (17.5.3 p. 329)
Forgive the inaccuracy of my vocabulary.
Anyway I'll try to implement what you have suggested.