Kőnig's lemma states that any *finitely-branching* tree with infinitely many nodes contains an infinite path. Weak Kőnig's lemma states the same thing about *binary* trees.

It's known that these are not equivalent over the base system $RCA_0$, but I'm struggling to see what goes wrong with the following construction:

- Take an arbitrary infinite finitely-branching tree $T$;
- Apply the Knuth transform to convert this into an equivalent binary tree $B$ on the same vertex-set;
- Use the statement of Weak Kőnig's lemma to find an infinite path $P = (x_1, x_2, x_3, \dots)$ in $B$.

Note that for each pair $(x_i, x_{i+1})$ of consecutive terms in $P$, $x_{i+1}$ is either a child or a sibling of $x_i$ when viewed as elements of $T$. We then define a subsequence which consists of only the terms $x_i$ such that $x_{i+1}$ is a child (rather than a sibling) of $x_i$. The resulting subsequence is then an infinite path in the original finitely-branching tree $T$.

Since this proof appears to be valid, my guess is that it's using something that can't be proved in $RCA_0$ (or indeed in $WKL_0$).