In this paper (pp 2-3) Friedman proves a version of Higman's Lemma for infinite sequences of finite words on a finite alphabet. Such a sequence $S$ is called "bad" if no element of $S$ occurs as a subsequence in a later element of $S$. (E.g., a sequence that contains $\dots,oar,\dots,foobar,\dots$ is not bad, because $oar$ occurs as a subsequence in the later word $foobar$.)
The proof begins by supposing (for the sake of contradiction) that there exists at least one bad sequence, then it constructs a so-called "minimal bad sequence" $y_1,y_2,y_3,\dots$ as follows:
- Choose $y_1$ to be a shortest word that starts some bad sequence, then
- choose $y_2$ to be a shortest word such that $y_1,y_2$ starts some bad sequence, then
- choose $y_3$ to be a shortest word such that $y_1,y_2,y_3$ starts some bad sequence, then
This would seem to be an evident use of the AoC, and the proof continues after merely remarking parenthetically that "The axiom of choice can be eliminated in an obvious way."
Question: In what "obvious way" can the AoC be eliminated from this proof? How can a (hypothetical) minimal bad sequence be constructed without the AoC?