 Friedman's finite form of Kruskal's theorem

For every natural parameter $k$, there is a finite length $N$ such that every sequence of $N$ finite rooted trees satisfying $|T_i|\le k+i$ has an earlier tree homeomorphically embedding into a later tree. It is a true finite-combinatorial principle unprovable in Peano arithmetic and in arithmetical transfinite recursion theory. Each fixed-parameter instance can still be verified by a sufficiently large finite search.