Gosh, minor graph embeddings brought back my PhD thesis, or rather the knowledge that the set of finite graphs is well-quasi-ordered did. I couldn't find the proof, but did find a paper on Kruskal's tree theorem for finite trees which pre-dates the same theorem for finite graphs.
I recommend C St. J A Nash-Williamns' paper if you want to understand the Kruskal Tree Theorem, as it is a model of clarity and exposition.
Sorry, just a bit of nostalgia. I'll shut up now.