Normal trees have faithful sequence representations

For each $t$, let $S_t$ be its immediate-successor set. With alphabet $A=T$, use the injection $e_t:S_t\to T$, $e_t(u)=u$. In the countable-successor case, the set $J_t$ of injections $S_t\to \omega$ is nonempty, including the empty map when $S_t$ is empty. All these maps lie in a set of relations contained in $T\times \omega$. Well-order that set and let $e_t$ be the least member of $J_t$. This is the sole use of AC; take $A=\omega$ in this case.

Define codes by recursion on levels. Give the root the empty code. At height $\beta +1$, the unique predecessor $t$ at height $\beta$ is the immediate predecessor of $u$; set $f(u)=f(t{)}^{⌢}⟨e_t(u)⟩$. At a nonzero limit height $\lambda$, put $f(u)={\bigcup }_{\beta <\lambda }f(u_{\beta })$, where $u_{\beta }$ is the unique height-$\beta$ predecessor. These are set-valued level operations, so transfinite recursion applies. On histories not satisfying the stated coherence condition the operation can be assigned the empty set; the next step proves that such histories never occur in the recursion.

By induction on the constructed level, $f(u)$ has domain $\mathrm{ht}(u)$ and restricts to $f(u_{\gamma })$ at every lower height $\gamma$. This is vacuous at the root. At a successor, appending one coordinate gives the domain and preserves all earlier restrictions. At a limit the earlier codes agree on overlaps by the induction assertion; their union is a function with domain the union of all smaller ordinals, namely that limit. Its restrictions are exactly the earlier codes.

The codes are injective on each level, again by induction. At zero there is just one root. At a successor, equality of codes gives equality of parent codes and hence of parents; equality of last coordinates then gives equality of the successors by injectivity of $e_t$. At a nonzero limit, equality of codes and step 3.1 give equal codes for each pair of predecessors; level injectivity below the limit makes all those predecessors equal. Thus the predecessor sets agree, and normality makes the two nodes equal.

Different levels give different code domains, so $f$ is injective on $T$. If $s{<}_{T}t$, step 3.1 identifies $f(s)$ with a proper restriction of $f(t)$. Conversely, if $f(s)$ is a proper initial segment of $f(t)$, take the predecessor $u$ of $t$ at height $\mathrm{ht}(s)$. Step 3.1 gives $f(u)=f(s)$, and step 4.1 gives $u=s$, hence $s{<}_{T}t$.

Every proper restriction of $f(t)$ is the code of its predecessor at that length, so the image is downward closed. The map onto its image is therefore the required order isomorphism and preserves heights by the domain computation. A height-one tree maps just to the empty sequence; no surjectivity onto all $A^{<\alpha }$ is needed.