Equality-preserving embeddings of finite trees For finite trees $T_{1}$ and $T_{2}$ labelled by elements of some infinite set $S$, (we may assume that $S=\mathbb{N}$ without loss of generality), we define an equality-preserving embedding $f$ to be an embedding of $T_{1}$ into $T_{2}$ in the usual graph-theoretical sense (i.e. a homeomorphism) with the extra condition that
$l_{1}(x)=l_{1}(y)$ implies $l_{2}(f(x))=l_{2}(f(y))$ for all vertices $x,y$ of $T_{1}$ (where $l_{1}$, $l_{2}$ are the labelling function for $T_{1}$ and $T_{2}$, respectively). We say that $T_{1}$ is an equalitiy-preserving minor of $T_{2}$, written $T_{1}\prec_{ep}T_{2}$ iff there is an equality-preserving embedding $f:T_{1}\rightarrow T_{2}$. 
(Note that we do not demand that differently labelled vertices are mapped to differently labelled vertices.)
Is $\prec_{ep}$ a well-quasi-ordering or even a better-quasi-ordering on the set of finite trees labelled by natural numbers? (This holds, of course, by Kruskal's theorem if we replace $S$ with a finite set.)
Edit: Considering only well-quasi-orderings for the moment, one can also model this as follows: Given a tree $T$, we introduce for each label $c$ a new vertex $v_{c}$, join it to all vertices of $T$ that have this label and forget about the labels. That makes the question almost an instance of the graph minor theorem (stating that the finite graphs are wqo under the minor relation) but for the fact that the embeddings must map extra vertices to extra vertices and tree vertices to tree vertices. This would follow if the graph minor theorem would continue to hold for graphs coloured with finitely many (in fact merely $2$) colours.
 A: I don't think your new model works. Consider two identical trees, $T_1$ and $T_2$. $T_1$ has a different colour at each vertex, and $T_2$ is monochromatic. Now $T_1 \preceq_{ep} T_2$ but the graph generated by $T_1$, which we can call $G_{T_1}$, is not a minor of $G_{T_2}$. You can fix the problem with your new statement by creating the new $v_c$ for each pair of equal vertices, rather than just for each colour.
The problem remains that the added vertices might be mixed up with the original vertices. I think you can fix this by duplicating each edge in the tree, at which point your done because, as you've said, the graph minor relation is a well-quasi-ordering by the Robertson-Seymour Theorem.
A: Somewhat surprisingly, the answer is in fact no, even for paths.  
Claim. There is an infinite antichain of coloured paths under $\prec_{ep}$.
Proof. Consider a path $P$ with $2k$ vertices, with vertices coloured from $[k]$.  The first $k$ vertices of $P$ are coloured $1, \dots, k$, in that order, and the remaining $k$ vertices are coloured $1, \dots, k$, but in an arbitrary order.  Thus, $P$ induces a permutation $\pi(P):[k] \to [k]$.  Now given two such paths, $P$ and $Q$, observe that $P \prec_{ep} Q$ if and only if $\pi(P) \leq \pi(Q)$, where $\leq$ is the containment relation on permutations. That is, $\pi_1 \leq \pi_2$ if we can obtain $\pi_1$ from $\pi_2$ by deleting elements of $\pi_2$ and then renaming elements appropriately. 
In this paper, Spielman and Bóna exhibit an infinite antichain of permutations, so we are done modulo a slight lie.  The slight lie is that a path may embed in another path with the opposite orientation.  However, we can fix this using two extra colours red and blue. We add three red vertices to the beginning of a path and four blue vertices at the end of a path.  This fixes the orientation, so we really are just working with the permutation order as claimed.  
This is joint with Luke Postle and Paul Wollan (possibly over beer). 
