Predicate macro

[mforets]

Would it be nice to have an macro like this?

@predicate x -> x > 1

@predicate x -> x \in X

or just @predicate x \in X, where X is a a lazy set, and similarly for the negated inclusion.
One can have more complicated predicates with and / or operators.