Rooted trees of finite sequences, levels, branches, and finite branching, with ordered finite successor sets

Let $\mathbb{N}$ be The natural numbers $\mathbb{N}$ (von Neumann). A rooted tree of finite sequences is a nonempty set $T$ of finite sequences of naturals such that the empty sequence belongs to $T$ and every initial segment of a member of $T$ also belongs to $T$.

The level $T_n$ consists of the sequences in $T$ of length $n$. A node $t^{⌢}a$ is an immediate successor of $t$ when it is obtained by appending $a\in \mathbb{N}$. The tree is finitely branching when each node has only finitely many immediate successors (The cardinality $\mid A\mid$ of a finite set). Their labels inherit the natural order of Order on the natural numbers, so every nonempty successor set has a least member.

An infinite branch is a function $b:\mathbb{N}\to \mathbb{N}$ such that the initial segment $(b(0),\dots ,b(n-1))$ lies in $T_n$ for every $n$. The empty initial segment is the root, and finite branching permits a node to have no successors; the hypotheses of an infinity lemma must rule out termination along the branch it constructs.