 Finite bad-sequence tree

Given a size bound with finitely many possible objects at each position, put finite bad sequences in a tree ordered by extension. The tree is finitely branching. Arbitrarily long bad sequences would give an infinite bad sequence by König infinity lemma. This compactness argument converts an infinite well-quasi-ordering theorem into a uniform finite length bound.