Variable-recycling count on a linear order

For a formula $\varphi (x)$ in $L^k$, $k\ge 2$, with only $x$ free, define $C_1^x=\varphi (x)$ and $C_{m+1}^x=\varphi (x)\wedge \exists y(x<y\wedge C_m^y)$. Obtain the superscript-$y$ formula by globally interchanging the two variable names in the superscript-$x$ version. Then $\exists x{C}_m^x$ counts at least $m$ distinct satisfying elements without introducing any further variable names. The recursion works on finite and infinite linear orders.