MSO + weak U

You all have already been disappointed that MSO+U is undecidable over infinite
words. Today, we will show that weakening U to a predicate U_1(X) holding if
the distance between two consecutive elements of X is unbounded, already leads
to undecidability (and actually, MSO+U_1 is as expressive as MSO+U). A
consequence is that adding a unary predicate UP(X) holding if X is ultimately
periodic to MSO also leads to undecidability.
This is a joint work with Mikolaj, Laure, Bruno and Sreejith.