 Solution

A well-quasi-ordering is a preorder $⪯$ in which every infinite sequence has $i<j$ with $x_i⪯x_j$. A sequence without such a pair is a bad sequence. We use rooted-tree homeomorphic embedding: an injective map of vertices preserving lowest common ancestors, so edges may become paths and a source root may map below the host root. Labels, when present, must increase in their label preorder. This convention is important; adjacency-preserving embeddings do not give the same theorem.

We first prove the auxiliary Higman lemma. If $Q$ is a well-quasi-order, its finite words are well-quasi-ordered by subsequence embedding with increased letters. Suppose not, and choose a minimal bad sequence of words: at each position choose one of least length among those permitting a bad continuation of the preceding prefix. No word is empty. Write $w_i=v_i{a}_i$ by deleting its last letter. A well-quasi-order has an infinite nondecreasing subsequence of any sequence: if no member of an infinite subsequence had infinitely many later upper bounds within it, one could recursively avoid the finitely many upper bounds of earlier choices and construct a bad sequence. Choose a member with infinitely many later upper bounds, restrict to those bounds and repeat. Apply this to get $a_{i_0}⪯a_{i_1}⪯\cdots$.

The sequence $w_0,\dots ,w_{i_0-1},v_{i_0},v_{i_1},\dots$ is still bad. An earlier prefix word embedding into a $v_{i_j}$ would embed into $w_{i_j}$, contrary to the original bad sequence. An embedding $v_{i_j}⪯v_{i_k}$ would extend by the comparable last letters to $w_{i_j}⪯w_{i_k}$, equally impossible. But its next word at position $i_0$ is strictly shorter than $w_{i_0}$, contradicting minimality. This proves Higman's lemma, including the possibility that a deleted word is empty, since that would make the proposed bad continuation impossible immediately.

We now prove the labelled version of Kruskal's tree theorem for labels in any well-quasi-order $Q$. Assume there is a bad sequence $T_0,T_1,\dots$, and choose one minimal in vertex count at each position, subject to bad extendibility. Let $\mathcal{S}$ be the collection of rooted subtrees obtained by deleting a root and taking one of its child branches, over all $T_i$.

This collection is well-quasi-ordered. Otherwise take a bad sequence $U_j$ from $\mathcal{S}$. Only finitely many of these objects can come from any bounded initial segment of the $T_i$, since that segment has only finitely many child branches and a bad sequence cannot repeat an object. Pass to a subsequence with $U_j$ a child branch of $T_{k_j}$ and $k_0<k_1<\cdots$. Thenis bad: a prefix tree embedding into $U_j$ would embed into $T_{k_j}$, and the $U_j$ are already bad among themselves. The next object $U_0$ has fewer vertices than $T_{k_0}$, contradicting the minimal bad choice. Notice that a child branch does embed into its full tree under the stated homeomorphic convention.

List each tree's child branches in any chosen order. The preceding result and Higman's lemma make these finite lists well-quasi-ordered. The product of two well-quasi-orders is well-quasi-ordered: first thin to an infinite nondecreasing subsequence in one coordinate and then find an increasing pair in the other. Therefore there are $i<j$ such that the root label of $T_i$ increases to that of $T_j$, and the child list of $T_i$ embeds as a subsequence into the child list of $T_j$, with each source branch homeomorphically embedding into its matched branch.

Map the root of $T_i$ to the root of $T_j$, and use these branch embeddings below it. Different child branches map into different host branches, so their lowest common ancestor maps to the host root. Within each branch it is preserved by the chosen embedding. Thus the whole map is injective, preserves all lowest common ancestors and respects labels, contradicting badness. Finite rooted trees labelled by a well-quasi-order are well-quasi-ordered under homeomorphic embedding. Taking one label proves Kruskal's tree theorem. If one uses a root-preserving convention, mark the root by a separate label incomparable with all ordinary labels and apply the labelled theorem; the marked root then has to map to the marked root. No adjacency-preservation assertion is being made.

For Friedman's finite form of Kruskal's theorem, fix $k\in \mathbb{N}$. The required finite conclusion isAssume there were arbitrarily long bad sequences satisfying these size bounds. Form the tree of their finite prefixes, using rooted-tree isomorphism classes as objects. At position $i$ only finitely many finite rooted trees have at most $k+i$ vertices, so this prefix tree is finitely branching and has nodes at arbitrarily large depths. König infinity lemma supplies an infinite branch: at each step some child must still have arbitrarily deep extensions, because there are only finitely many children. The branch is an infinite bad sequence of finite rooted trees, contradicting Kruskal's theorem. Thus such an $N$ exists. The argument also works for any prescribed size-bound function, or any fixed finite label set, because each position then still has finitely many possible objects.