A nonempty countable set has a padded enumeration in ZF

Assume $D$ is nonempty and at most countable; by [L1] it suffices to produce a surjection $\mathbb{N}\to D$ explicitly from the two alternatives of [L2].

Case 1: assume $D$ is countably infinite, so that there is a bijection $e:\mathbb{N}\to D$; case 2: assume $D$ is finite, so that there is $m\in \mathbb{N}$ with a bijection $e:m\to D$.

In case 1, take $s:=e$; it is a function $\mathbb{N}\to D$ and it is surjective, so its range is $D$; no choice was used, since $e$ was already given.

In case 2, since $D$ is nonempty and $e:m\to D$ is bijective, $m\mathrm{\ne }0$: otherwise $D\approx m=0=\mathrm{\varnothing }$ by [L3], contradicting that $D$ has an element.

In case 2, continuing, define $s:\mathbb{N}\to D$ by the two clauses $s(n):=e(n)$ for $n\in m$ and $s(n):=e(0)$ for $n\in \mathbb{N}\setminus m$; this is well defined because $m=\{0,\dots ,m-1\}$ and $0\in m$ by step 2.2 and [L3], so $e(0)\in D$ is available as the constant value.

In case 2, continuing, $s$ has range $D$: if $d\in D$ then $d=e(k)$ for some $k\in m$ because $e$ is surjective, and then $s(k)=e(k)=d$ by step 3.1; conversely every value of $s$ is a value of $e$, hence lies in $D$.

Every nonempty at most countable $D$ therefore falls under case 1 or case 2 and is the range of the explicitly defined sequence $s$ of step 2.1 or of step 4.1; no choice principle was used in either case.