A good reference for the theorem is the paper by Jean H. Gallier, "What's so special about Kruskal's theorem and the ordinal $\Gamma_0$? A survey of some results in proof theory." Ann. Pure Appl. Logic 53 (1991), no. 3, 199-260.
(With a short erratum in Ann. Pure Appl. Logic 89 (1997), no. 2-3, 275.)
I do not know of any (undergraduate) books where Friedman's result is discussed in any sort of detail, but this paper is very good.
For some background, you may also want to read the paper by Joseph B. Kruskal, "The theory of well-quasi-ordering: A frequently discovered concept." J. Combinatorial Theory Ser. A 13 (1972), 297–305.
Here is the review from MathScinet:
MR0306057 (46 #5184)
This is a survey paper outlining the history and present state of the theory of well-quasi-ordered sets. A wqo is a qo in which each strictly descending sequence is finite and each set of pairwise incomparable elements is finite or, equivalently, each nonempty subset has one but no more than a finite number of nonequivalent minimal elements. If $s$ and $t$ are sequences from a wqo set then $s\leq t$ means that some subsequence of $t$ majorizes $s$ term by term. A basic question is: when is a set of sequences from a wqo set itself wqo? The author traces the history of this problem and points out that over the years many of the results have been rediscovered and republished. This paper and this section in MR should help eliminate further duplication of these results.
Reviewed by P. F. Conrad
A good book to learn about well-quasi-ordering theory itself, from a logician's perspective, is "Recursive Aspects of Descriptive Set Theory" (Oxford Logic Guides), by Richard Mansfield and Galen Weitkamp. I think the level is fairly accessible. The chapter on wqo theory is by S. Simpson, who is a very good expositor.