Higman lemma ($Q^{\ast }$)

If $Q$ is a well-quasi-ordering, its finite words form a well-quasi-ordering under subsequence embedding with coordinatewise increase of letters. A minimal bad sequence proof removes the last letter of selected words whose last letters form a nondecreasing subsequence, then contradicts minimality. The result implies finite-subset lifting of a well-quasi-order under Hoare domination preorder.