### Abstract

- If the sets A and B are wqo then their Cartesian product is wqo.
- If the set A is wqo then the set of finite lists over A is wqo.
- If the set A is wqo then the set of finite trees over A is wqo.

### Change history

[2012-06-11] Added Kruskal's Tree Theorem.

[2012-12-19] New variant of Kruskal's tree theorem for terms (as opposed to
variadic terms, i.e., trees), plus finite version of the tree theorem as
corollary.

[2013-05-16] Simplified construction of minimal bad sequences.

[2014-07-09] Simplified proofs of Higman's lemma and Kruskal's tree theorem,
based on homogeneous sequences.

[2016-01-03] An alternative proof of Higman's lemma by open induction.

[2017-06-08] Proved (classical) equivalence to inductive definition of
almost-full relations according to the ITP 2012 paper "Stop When You Are
Almost-Full" by Vytiniotis, Coquand, and Wahlstedt.