Weak MSO+U with path quantifiers

Over infinite trees, satisfiability is decidable  for weak monadic second-order logic extended by the unbounding quantifier U and  quantification over infinite paths. The proof is by reduction to emptiness for a certain automaton model, while emptiness for the automaton model is decided using profinite trees.