  We prove that the MSO+U logic is compositional in the following sense:
whether an MSO+U formula holds in a tree T depends only on MSO+U-definable
properties of the root of T and of subtrees of T starting directly below the
root. Another kind of compositionality follows: every MSO+U formula whose all
free variables range only over finite sets of nodes (in particular, whose all
free variables are first-order) can be rewritten into an MSO formula having
access to properties of subtrees definable by MSO+U sentences (without free
variables).

Logic in Computer Science