Let $\mathfrak{g}$ be the Lie algebra of a Lie group $G$ which acts on a manifold $M$. It is quite standard that the basic forms in $\Omega^*(M) \otimes W(\mathfrak{g}^*)$ form a model for the singular equivariant cohomology of $M$. However, I have never seen a proof and it is not straightforward to me. Could someone give a sketch or a reference of the proof of this fact? It is probably in one of Cartan's papers but I haven't been able to find it.
Here goes some background:
We define its Weil algebra by $W^*(\mathfrak{g}^*)=S^*(\mathfrak{g}^*) \otimes \wedge^*(\mathfrak{g}^*)$ there is also a natural differential operator $d_W$ which makes $W*(\mathfrak{g}^*)$ into a complex. We define $d_W$ as follows:
Choose a basis $e_1,...,e_n$ for $\mathfrak{g}$ and let $e^*_1,...e^*_n$ its dual basis in $\mathfrak{g}^*$. Let $\theta_1,...,\theta_n$ be the image of $e^*_1,...e^*_n$ in $\wedge(\mathfrak{g}^*)$ and let $\Omega_1,...,\Omega_n$ be the image of $e^*_1,...e^*_n$ in $S(\mathfrak{g}^*)$. Let $c_{jk}^i$ be the structure constants of $\mathfrak{g}$, that is $[e_j,e_k]=\sum_{i=1}^nc_{jk}^ie_i$. Define $d_W$ by \begin{eqnarray} d_W\theta_i=\Omega_i- \frac{1}{2}\sum_{j,k} c_{jk}^i \theta_j \wedge \theta_k \end{eqnarray} and \begin{eqnarray} d_W\Omega_i=\sum_{j,k}c_{jk}^i\theta_j \Omega_k \end{eqnarray} and extending $d_W$ to $W(\mathfrak{g})$ as a derivation.
We can also define interior multiplication $i_X$ on $W(\mathfrak{g}^*)$ for any $X \in \mathfrak{g}$ by \begin{eqnarray} i_{e_r}(\theta_s)=\delta^r_s, i_{e_r}(\Omega_s)=0 \end{eqnarray} for all $r,s=1,...,n$ and extending by linearity and as a derivation.
Now consider $\Omega^*(M) \otimes W(\mathfrak{g}^*)$ as a complex. Using this definition of interior multiplication, together with the usual definition of interior multiplication on forms, we define the basic complex of $\Omega^*(M) \otimes W(\mathfrak g^*)$:
We call $\alpha \in \Omega^*(M) \otimes W(\mathfrak{g}^*)$ a basic element if $i_X(\alpha)=0$ and $i_X(d \alpha)=0$. Basic elements in $\Omega^*(M) \otimes W(\mathfrak{g}^*)$ form a subcomplex which we denote by $\Omega^*_G (M)$.
The claim is that $H^*(\Omega^*_G (M))=H^*(M \times_G EG)$ where the right hand side denotes the singular equivariant cohomology of $M$.
