Let $A$ be a set equipped with a well-founded relation $<$, let $LA$ be the set of finite lists of elements of $A$, and define a relation $\prec$ on $LA$ such that $\ell \prec m$ if $\ell$ is obtained from $m$ by replacing some element $x\in A$ occurring in $m$ with some finite list (perhaps empty) whose elements are all $<x$. For example, if $A=\mathbb{N}$ with its usual ordering, then in $LA$ we would have

$ (1,3,4,2,0) \prec (1,5,0) $

and also

$ (1,0) \prec (1,5,0) .$

In classical mathematics, I can prove that $(LA,\prec)$ is also well-founded, as follows. Suppose we had an infinite sequence $\cdots \ell_3 \prec \ell_2 \prec \ell_1$, and define a tree $T$ whose vertices are pairs $(n, x\in \ell_n)$ and whose edges are induced by the definition of $\prec$. That is, if we had $ \ell_2 = (1,3,4,2,0) \prec (1,5,0) = \ell_1 $ then there would be edges $(1,0) \to (2,0)$ and $(1,1) \to (2,1)$ and $(1,5) \to (2,3)$ and $(1,5) \to (2,4)$ and $(1,5) \to (2,2)$. Now exclude from $T$ all the trivial infinite branches (those whose second component is constant). By Konig's lemma, the resulting subtree $T'$ still has an infinite branch. This yields an infinite descending sequence in $A$, a contradiction.

This argument is nonconstructive in two ways: it uses the equivalence of well-foundedness with the nonexistence of infinite descending sequences, and it uses Konig's lemma. Is there a constructive proof that $(LA,\prec)$ is well-founded?