Are these notions of strongly equivariant D-modules equivalent?

It seems that there are two notions of strongly equivaraint $D_X$- Modules and I would like to know if they are equivalent, or at least how they are related. Let $\rho: G\times X \rightarrow X$ be an action of an algebraic group on a smooth variety over the complex numbers. The first definition goes like this:

An equivariant $D_X$ Module is just a $D_X$ module $M$ together with an isomorphism $$\rho^* M\rightarrow \pi^* M$$ of $D_{G\times X}$ -modules. That isomorphism has to satisfy some cocycle condition.

The other definition is a bit more cumbersome to write down. First it requires just an isomorphism of $O_{G\times X}$ modules, not necessarily of $D_{G\times X}$-modules $$\rho^* M\rightarrow \pi^* M$$ modules, which again satisfies the cocycle conditon. In addition it requires the action map $$D_X\otimes M \rightarrow M$$ to be equivariant. Finally there is another condition to be satisfied: Observe that we get two operations of the liealgera on $M$:

One operation, by directly differentiating the action of $G$ on $M$.

Another operation in the following way: First we differentiate the action of $G$ on $X$, and get a map $$Lie(G)\rightarrow Der_X$$ from the liealgebra into vectorfields on $X$. Because $M$ is a $D_X$ module we can compose this map with the action of vectorfields on $M$ and get our second operation.

We require these operations to coincide.

A more precise definition of the second kind is given here on pages 48-49: http://www.math.harvard.edu/~gaitsgde/267y/catO.pdf

So the question is, are these two notions equivalent?

Edit: If anybody else needs these facts, I found a reference which gives a proof: http://alpha.uhasselt.be/Research/Algebra/Publications/Geq.ps

-

More precisely, there are two ways to think of D-modules on a stack $X/G$ (aka $G$-equivariant D-modules on $X$). First, you can just describe them by descent from $X$ -- the descent data is exactly your first description - the two pullbacks have to agree, in a way that's associative. The same description works for the (dg) derived category of D-modules on the stack $X/G$ -- you make the simplicial scheme with simplices $G\times G\times\cdots\times G\times X$, and take the (homotopy) limit of the dg categories of $D$-modules on the simplices. Again this is explicitly in BD chapter 7, as well as in the appendix to the long paper by Frenkel-Gaitsgory and in my Character Theory paper with Nadler.
The second description is quantum hamiltonian reduction (aka BRST). You can write the cotangent of $X/G$ as the quotient by $G$ of the zero fiber of the moment map on $T^* X$. Now quantize, you can write the quantum version of $T^*(X/G)$ --- ie D-modules on $X/G$ - by first taking G-equivariants as O-modules (this gives the quantization of $(T^*X)/G$) and then imposing the zero value of the moment map, which means the compatibility of Lie algebra actions you wrote. This picture is also in BD..and again if you take invariants and coinvariants (ie impose 0 moment value) in a derived way the statement holds on the derived level.
One way Nadler and I like to say this is by thinking about D-modules as O-modules on the de Rham space $X_{dR}$ (quotient of X by formal neighborhood of the diagonal). Then D-modules on $X/G$ means O-modules on the de Rham space of $X/G$, which is $X_{dR}/G_{dR}$ -- spelling that out gives the first description you wrote. To get the second picture, you first impose $G$-equivariance as an $O$-module, which means looking at $X_{dR}/G$. But $G_{dR}=G/\widehat{G}$ (formal group of $G$) is a very useful realization -- ie Lie groups DO have canonical normal "subgroups"!).. the second step, fixing the action of the Lie algebra (or equivalently the formal group) tells you which sheaves on $X_{dR}/G$ actually come from $X_{dR}/G_{dR}$, ie are strongly equivariant..