Labelled version of Kruskal's tree theorem
= Labelled version of Kruskal's tree theorem
Finite <rooted trees> labelled in a <well-quasi-ordering> are a <well-quasi-ordering> under <label-monotone tree embedding>. A <minimal bad sequence> argument makes the collection of proper rooted subtrees a <well-quasi-ordering>; <Higman lemma> then compares their child lists while the root labels are compared in the label order.