  The famous theorem of Higman states that for any well-quasi-order (wqo) $Q$
the embeddability order on finite sequences over $Q$ is also wqo. In his
celebrated 1965 paper, Nash-Williams established that the same conclusion holds
even for all the transfinite sequences with finite range, thus proving a far
reaching generalization of Higman's theorem.
  In the present paper we show that Nash-Williams' Theorem is provable in the
system $\mathsf{ATR}_0$ of second-order arithmetic, thus solving an open
problem by Antonio Montalb\'an and proving the reverse-mathematical equivalence
of Nash-Williams' Theorem and $\mathsf{ATR}_0$. In order to accomplish this, we
establish equivalent characterization of transfinite Higman's order and an
order on the cumulative hierarchy with urelements from the starting wqo $Q$,
and find some new connection that can be of purely order-theoretic interest.
Moreover, in this paper we present a new setup that allows us to develop the
theory of $\alpha$-wqo's in a way that is formalizable within
primitive-recursive set theory with urelements, in a smooth and code-free
fashion.
