Graph minors XXIII. Nash-Williams' immersion conjecture

We define a quasi-order of the class of all finite hypergraphs, and prove it is a well-quasi-order. This has two corollaries of interest:
• Wagner's conjecture, proved in a previous paper, states that for every infinite set of finite graphs, one of its members is a minor of another. The present result implies the same conclusion even if the vertices or edges of the graphs are labelled from a well-quasi-order and we require the minor relation to respect the labels.
• Nash-Williams' “immersion” conjecture states that in any infinite set of finite graphs, one can be “immersed” in another; roughly, embedded such that the edges of the first graph are represented by edge-disjoint paths of the second. The present result implies this, in a strengthened form where we permit vertices to be labelled from a well-quasi-order and require the immersion to respect the labels.