Lambda calcul et point fixe

[jingenbl]

Bonjour et bonne année 2021 (meilleure que la précédente!)
Je suis novice en -calcul et je rame un peu (beaucoup)...
Il existe un théorème du point fixe:
" il existe un combinateur tel que "

Admettons.
Il en découle le corollaire suivant:
pour tout et l'équation

peut être résolue en . C'est-à-dire qu'il existe tel que

Il suffirait de prendre

Mais justifications tournent en boucle...Sans doute ma compréhension est trop faible, mais je ne vois pas...
Merci de vos explications et/ou éclairage