Letting $EG$ be the total space of some group $G$, and $f: X \to Y$ a $G$-equivariant map with $X$ a free $G-CW$ complex, we can form the bundle $p^{\prime}:EG \times_G (X \times Y) \to EG \times_{G} X: [e,(x,y)] \to [e,x]$. The claim is that projection onto the second factor mod $G$ (i.e $\pi_2/G$) is a in fact a homotopy equivalence of bundles between $p^{\prime}$ and $p:X \times_G Y \to X/G:[x,y] \mapsto [x]$
The way I see it, there is the map $\pi_2/G:EG \times_G(X \times Y) \to X \times_G Y$ and $\pi_2/G:EG \times_G X \to X/G$ fit into a square diagram, and a bundle homotopy equivalence is saying that the classifying map $g^{\prime}$ for $p^{\prime}$ is homotopy equivalent to $(\pi_{2}/G) \circ g$, where $g$ is the classifying map for $p$.
Question $1$: Is there a better way of seeing what this means heuristically/ how does this induce a bijection of sections between the two bundles?
Question $2$: How can we prove that this is a homotopy equivalence? Since $EG$ is weakly contractible, I can see how we should be able to find some appropriate exact sequence (of fibration) to use witehead's theorem for $\pi_2/G:EG \times_G X \to X/G$ somewhere.
A reference can be found here on page 67
Since $X$ is a free $G$-space the projection $p_X:EG\times_G X\rightarrow X/G$ is a fibration with fibre $EG$. Since $EG$ is weakly contractible this fibration is a weak equivalence, and since $X$ is a CW complex, it is in fact a homotopy equivalence. The fact that $X$ is $G$-free also means that $X\times Y$ is $G$-free, and hence the same reason applies to get a fibration $p_{X\times Y}:EG\times_G(X\times Y)\rightarrow X\times_GY$ which is also a homotopy equivalence.
Moreover the composition $EG\times_G(X\times Y)\xrightarrow{p'}EG\times_GX\xrightarrow{p_X}X/G$ factors over $p_{X\times Y}$ to give the map $p:X\times_GY\rightarrow X/G$. Putting these maps together gives a strictly commutative square diagram which is easily seen to be a pullback using the fact that the induced maps of fibres are easily verified to be homeomorphisms. The square defines a bundle map, and since $p$, $p'$ are homotopy equivalences we get that $p$, $p'$ define a homotopy equivalence of bundles.
The fact that the previously assembled square is a pullback gives you the bijection between the sections of $p$ and $p'$.