We give a (to the best of our knolwdge) new proof of the celebrated result by Nash-Williams that if Q is wqo, then the sequences with finite range ordered by embeddability also form a wqo. We will then proceed to show that this proof can be formalized in ATR0: as we will see, an important ingredient for this is another concept from infinitary combinatorics, namely that of bqo (introduced by Nash-Williams).
Joint work with Fedor Pakhomov