I'm contemplating the proof of Kruskal's Tree Theorem, as presented in the book "Term Rewriting and All That." They use it to prove that every simplification order is well-founded: first by showing that the homeomorphic embedding is a wpo, and then by showing that every simplification order contains the homeomorphic embedding.
It seems to me that the only properties they use of the homeomorphic embedding in the proof are that it's well-founded, and that each term is > its subterms -- exactly the property that defines a simplification order. Does the same proof work if I instead use an arbitrary simplification order*? Does this mean every simplification order is a well-partial order*?
*One caveat: restricting terms to a finite set of variables, because it's trivial to construct a counterexample with an infinite set of variables.