In Hindley (Lambda-Calculus and Combinators, an Introduction), Corollary 3.3.1 to the fixed-point theorem states:
In $\lambda$ and CL: for every $Z$ and $n \ge 0$ the equation $$xy_1..y_n = Z$$ can be solved for $x$. That is, there is a term $X$ such that $$Xy_1..y_n =_{\beta,w} [X/x]Z$$
I dont understand how to even think about it. I was thinking that $y_1...y_n$ could be thought of as a function on which $X$ acts so $X$ is the fixed point I would like to find. Is that right?
And I dont even understand the proof a little bit, which is - Choose $X = \mathbf{Y}(\lambda x y_1...y_n.Z)$ What does it mean? How is it a solution? Can someone explain?
Note that $\mathbf{Y}$ here means any fixed-point combinator, i.e. $\mathbf{Y}X =_{\beta, w}X$ for any expression $X$.