The TRASI we construct for proving Lemma REF  has to handle \(\mathrm {MSO} (<_1)\)  formulas occuring in constraints. To do so, it will store type-information of nodes. Recall that a \(k\) -ary \(\mathrm {MSO}\) -type \(\tau (x_1, \ldots , x_k)\)  of quantifier-rank \(q\)  is a maximal consistent conjunction of \(\mathrm {MSO}\) -formulas of quantifier-rank \(q\)  and free variables \(x_1, \ldots , x_k\)  (see [1]} for background on \(\mathrm {MSO}\) -types). For a tree \(t\)  with ancestor order \(<\)  and an \(\mathrm {MSO} (<)\) -type \(\tau \) , we write \((t, u_1, \ldots , u_k) \models \tau \)  if the tuple \((u_1, \ldots , u_k)\)  of nodes in \(t\)  is of type \(\tau \) .
