Let $(A,\prec)$ be a set with a well founded relation. Then let

• $(L A,\prec)$ be the set of (finite) lists from $A$ together with the relation that Mike defines above and

• $(K A,\prec)$ be the set of Kuratowski-finite subsets of $A$ together with the relation

$$ U\prec V \quad\equiv\quad (\exists v\in V.\top) \ \land\ (\forall u\in U. \exists v\in V. u\prec v). $$

My definition explicitly requires $V$ to be inhabited; the same is also implicit in the wording of Mike's definition.

Then the obvious map $L A\to K A$ preserves $\prec$: it takes Mike's relation to mine.

The constructive proof that $(K A,\prec)$ is well founded is given in Prop 8.6 of my paper Intuitionistic Sets and Ordinals, JSL 61 (1996) 705-744. It is the "box" proof displayed on page 737 in the journal.

It follows (easily) that $(L A,\prec)$ is well founded too (Prop 1.7(a)).

Let $(A,\prec)$ be a set with a well founded relation. Then let

• $(L A,\prec)$ be the set of (finite) lists from $A$ together with the relation that Mike defines above and

• $(K A,\prec)$ be the set of Kuratowski-finite subsets of $A$ together with the relation

$$ U\prec V \quad\equiv\quad (\exists v\in V.\top) \ \land\ (\forall u\in U. \exists v\in V. u\prec v). $$

My definition explicitly requires $V$ to be inhabited; the same is also implicit in the wording of Mike's definition. This excludes $\emptyset\prec\emptyset$.

Then the obvious map $L A\to K A$ preserves $\prec$: it takes Mike's relation to mine.

The constructive proof that $(K A,\prec)$ is well founded is given in Prop 8.6 of my paper Intuitionistic Sets and Ordinals, JSL 61 (1996) 705-744. It is the "box" proof displayed on page 737 in the journal.

It follows (easily) that $(L A,\prec)$ is well founded too (Prop 1.7(a)).