This is exercise 2.10(iii) from "Introduction to Lambda Calculus". We need to find an $F$ such that $F \mathbf{I} \mathbf{K} \mathbf{K} = F \mathbf{K}$
Here there is my solution:
Let $\mathbf{K}_3 \equiv \lambda xyabz.xyz$ and let $F \equiv \mathbf{Y} \mathbf{K}_3$. We have that $$\mathbf{Y}\mathbf{K}_3 = \mathbf{K}_3 (\mathbf{Y} \mathbf{K}_3) = (\lambda xyabz.xyz)\mathbf{Y} \mathbf{K}_3 = \lambda abz. \mathbf{Y} \mathbf{K}_3 z.$$
Thus, $F \mathbf{I} \mathbf{K} \mathbf{K}=(\mathbf{Y} \mathbf{K}_3)\mathbf{I} \mathbf{K} \mathbf{K} = (\lambda abz. \mathbf{Y} \mathbf{K}_3 z) \mathbf{I} \mathbf{K} \mathbf{K} = (\lambda z. \mathbf{Y} \mathbf{K}_3 z) \mathbf{K} = \mathbf{Y} \mathbf{K}_3 \mathbf{K} = F \mathbf{K}$.
I think it is correct, but I am really not sure for three reasons:
it really looks ugly;
it is not 'unique', since $\mathbf{K}_3$ can be alternatively defined as $\mathbf{K}_3 \equiv \lambda xyazb.xyz$;
it is completely independent from the combinators, since it can work for any term.
Are my concerns correct?
Is the solution correct?
If it is, is there a more pleasing solution?
If not, what's wrong with it?
Any feedback will be greatly appreciated.
Thank you for your time.
PS: Of course, $\mathbf{K}_3$ is just the name I gave to that term (i.e., it is not official).