it is not true in general that the cokernel of $\partial_n$ acting on $M$ is a holonomic ${\mathcal{D}}_{n-1}$-module, which makes the proof more difficult. The kernel of $\partial_n$ is again holonomic, and the cokernel is holonomic whenever $M$ satisfies a certain generic condition called *$x_n$-regularity*. It turns out that if $M$ is holonomic, we can always make a linear change of coordinates (which does not affect de Rham cohomology) after which $M$ becomes $x_n$-regular. The same routine induction argument used by Bernstein is then sufficient to prove finiteness of the de Rham cohomology in the formal power series case as well:

[@essen Prop. 2.2]\[mainthm\] Let $k$ be a field of characteristic zero, let $R = k[[x_1, \ldots, x_n]]$ be a formal power series ring over $k$, and let ${\mathcal{D}}= {\mathcal{D}}(R,k)$ be the ring of $k$-linear differential operators on $R$. If $M$ is a holonomic left ${\mathcal{D}}$-module, its de Rham cohomology spaces $H^i_{dR}(M)$ are finite-dimensional over $k$ for all $i$.

Van den Essen’s proof is not contained in a single paper. The complete argument requires results from at least five of his papers, as well as his (unpublished) thesis. Moreover, some of the necessary results are proved more than once in 