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.