>>26
もろもろ，ありがとうございます．

早速その `Introduction to Lambda Calculus'
http://citeseer.ist.psu.edu/barendregt94introduction.html
なのですが，p.12 の 2.13 の例 (i) でいきなりつまずいています．
この例のココロもピンと来ないのですが，とくに以下の部分がわか
りません．

∃G∀X GX = SGX が成り立つことを，
∀X GX = SGX <= Gx = SGx　　　　　…(1)
　　　　　　 <= G = λx.SGx　　　 …(2)
　　　　　　 <= G = (λgx.Sgx)G　 …(3)
　　　　　　 <= G ≡ Y(λgx.Sgx)　…(4)

として示そうとしていますが，(3) と (4) の間の変換はなぜ
こうなるのでしょうか?
ここで X は任意のλ式で，
S ≡ λxyz.xz(yz)
Y ≡ λf.(λx.f(xx))(λx.f(xx))
だと思います．