Solution (source code)

= Solution

A <well-quasi-ordering> is a <preorder> $(Q,\le)$ such that every infinite <sequence> $(x_n)$ has indices $i<j$ with $x_i\le x_j$. Reflexivity and transitivity are part of the definition; antisymmetry is unnecessary. An infinite <sequence> without such a pair is a <bad sequence>.

The <perfect subsequence lemma> strengthens this definition: \b[every infinite <sequence> in a <well-quasi-order> has an infinite nondecreasing <subsequence>], meaning
$$
\boxed{i_0<i_1<\cdots,\qquad x_{i_r}\le x_{i_s}\quad(r<s).}
$$
Here is a proof that does not assume the lemma implicitly. There must be an index $i$ with infinitely many later indices $j$ satisfying $x_i\le x_j$. Otherwise each index would have only finitely many such successors. Starting with any index, choose the next one beyond the <union> of those finite successor <sets> for the previously chosen indices. This constructs a <bad sequence>, contradicting the <well-quasi-ordering> property.

Choose $i_0$ with infinitely many successors above it, and restrict to those successors. Apply the same argument to that infinite <subsequence>, obtaining $i_1>i_0$ with infinitely many later successors above it within the restricted <sequence>. Continue. Every subsequent restriction lies inside all previous upper cones, so $x_{i_r}\le x_{i_s}$ for every $r<s$. This proves the lemma, including for a genuine <quasi-order> with distinct equivalent elements. Both alternatives below use it.