Minimal bad sequence
= Minimal bad sequence
A minimal bad sequence chooses each successive object of least possible natural-number size among choices that admit an infinite bad continuation of the already fixed prefix. Replacing its next object by a strictly smaller one cannot leave a <bad sequence>. This contradiction principle proves <Higman lemma> and the <labelled version of Kruskal's tree theorem>.