# Trying to verify the solution to a lambda calculus equation

I am going through the following introduction to lambda calculus :

http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf

At page 12 , the following has been asked to prove

$\exists$ $G$ $\forall X$ such that

$GX$ = $GG$

This means to find a function which takes a function as an argument and returns the same expression irrespective of the function .

The book posits the solution to be $G$ = $Y$ $( \lambda gx. gg)$

On trying to verify this I first evaluated the L.H.S to be

$GX$ = $Y ( \lambda gx.gg )$ $X$.

Now $X$ being the argument will be picked up by the first bound variable so .

$L.H.S$ = $Y ( \lambda x . XX)$ = $( \lambda x . XX)$ $Y ( \lambda x . XX)$ = $Y ( \lambda x .$ $Y ( \lambda x . XX)$ $Y ( \lambda x . XX)$)

Here due to the presence of the form $YF$ , I can carry on the reduction continuously by replacinf $YF$ with $FYF$