 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.