The monadic description of derived D-modules for derived affine schemes

Let $A \in \CAlg^{ \cn, \lfp }_{ \C }$ be possibly unbounded, let $\g \in \LieAlgbd_{ A }$, and let $\MC(\g)$ be the formal moduli problem under $\Spec A$ associated to $\g$. The category $\IndCoh_{ 0 }(\MC(\g)/A)$ is defined as in Beraldo's construction.

Derived D-module equivalence. There exists a symmetric monoidal equivalence

$$\IndCoh_{ 0 }(\MC(\g)/A) \stackrel{\sim}{\longrightarrow} \LMod_{ U(\g) }.$$

This extends the known bounded case to possibly unbounded derived affine schemes. The claim concerns the compatibility between the ind-coherent definition of derived D-modules and representations of the universal enveloping algebra; the source says that the associated formal moduli problem should be used even though the relevant correspondence is not an equivalence.