I know that $K_G (X \times EG) =K(X \times_G EG)$. I've seen the proof that this is the case for the vector space definition of K-theory, but I wanted one that works for the definition where $K_G(X)= [X, F(H)]_G$ for $H$ a $G$-universe (infinite sum of all irreducible reps) and $F(H)$ the fredholm operators on $H$. It seems to me that the easiest way to show this is to use sections, ie: $$ [X \times EG, F(H)]_G = \Gamma [ (X \times EG)\times_G F(H) \to X \times_G EG ] $$ then to somehow trivialize the $(X \times EG)\times_G F(H) \to X \times_G EG$ bundle.
I know $F(H) \times_G EG \to F(H) \times_{U(H)} EG \tilde{\to} F(H)$, where $U(H)$ is the unitary transformations on $H$, this is contractible by Kuiper's theorem and thus itself a model for EU and since $H$ is faithful then it is also a model for $EG$. So the first map is modding out by the action of $U$, the second is the isomorphism induced by evaluation. Maybe this is helpful?
The two maps are: $$ \alpha: (X \times EG) \times_G F(H) \to X \times_EG EG \times F(H) $$ $$ \alpha([x,e,f] = [x,e],e^{-1}f $$ and $$ \beta: X \times_G EG \times F \to (X \times EG) \times_G F(H) $$ $$ \beta([x,e],f)=[x,e,ef] $$ Easy to check that they work.