Finite bad-sequence tree
= 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.