 Solution

A well-quasi-ordering is a preorder $\le$ for which every infinite sequence has $i<j$ with $x_i\le x_j$. Such a comparable pair is good; a sequence without one is a bad sequence. Equivalently there is no infinite strictly descending chain in the quotient order and no infinite antichain.

A better-quasi-ordering strengthens this by requiring every barrier array to be good. A barrier in better-quasi-order theory on an infinite $A\subseteq \omega$ is a family $B$ of nonempty finite increasing sequences, no one properly contained in another, such that every infinite subset of $A$ has an initial segment in $B$. Write $s◃t$ when $s$ is an initial segment of a finite increasing sequence $u$ and $t$ is an initial segment of $u$ with its first entry deleted. A map $f:B\to Q$ is good if some $s◃t$ satisfy $f(s)\le f(t)$. Requiring this for all barriers defines a better-quasi-ordering. Singleton barriers recover well-quasi-ordering; the stronger property supports infinitary closure operations that can fail for a mere well-quasi-ordering.

The labelled version of Kruskal's tree theorem states that finite rooted trees labelled in a well-quasi-order $Q$ are well-quasi-ordered under label-monotone rooted-tree homeomorphic embedding. An embedding sends edges to nonempty downward paths, separates different child branches, and increases labels. Initially allow the source root to land at any vertex of the target. We prove this version; forcing roots to match follows at the end.

Suppose there is a bad sequence $T_0,T_1,\dots$. Choose it as a minimal bad sequence: at each stage choose a tree with the fewest vertices among those admitting a bad continuation of the already fixed prefix. Let $U$ contain all proper rooted descendant subtrees of these trees. We first show that $U$ is well-quasi-ordered by the same root-flexible embedding.

Otherwise choose a bad sequence $S_0,S_1,\dots$ from $U$. Each finite collection of the $T_n$ has only finitely many descendant subtrees, and a bad sequence cannot repeat an object. Thus, after passing to a subsequence, choose strictly increasing $n_i$ such that $S_i$ is a proper descendant subtree of $T_{n_i}$. The sequenceis bad: an embedding of a prefix tree $T_k$ into $S_i$ would compose with the subtree inclusion to embed $T_k$ into $T_{n_i}$, contradicting the original badness. But $S_0$ is smaller than $T_{n_0}$, contradicting minimality. Hence $U$ is well-quasi-ordered.

Give the children of each root any fixed linear order, and describe a tree by its root label and the word of its child subtrees. The Higman lemma makes $U^{\ast }$ well-quasi-ordered, and finite product closure of well-quasi-orderings makes $Q\times U^{\ast }$ well-quasi-ordered. There are therefore $i<j$ with an increased root label and an embedding of the child word of $T_i$ as a subsequence of that of $T_j$. Embed the root into the root, use the chosen subtree embeddings inside the corresponding distinct target branches, and join their root images to the target root by downward paths. This gives a label-monotone tree embedding $T_i\to T_j$, the required contradiction.

If root-preserving embeddings are required, replace $Q$ by the disjoint union of two copies of $Q$, label every root in copy one and every other vertex in copy zero, and allow comparisons only within a copy. This is again a well-quasi-order. The unique copy-one vertex of a tree forces an embedding to send root to root. Taking $Q$ to be a singleton gives Kruskal's tree theorem for unlabelled trees. The Higman lemma used above follows from the same minimal-bad-sequence argument for words: delete the last letters along an infinite nondecreasing subsequence of those letters; a good pair among the shortened words would extend to a good pair of original words, contradicting minimality. Empty shortened words cause an immediate good pair. This supplies the word lemma needed in the tree proof.