Lemma A1.8

$x,y$ を bound させて α0-contraction と α-contraction とのギャップを埋めている、ということだろうか。

A1.7 の $M^\prime$ を取り出して、$λx.M \rhd_{\alpha0} λx.M^\prime$ と言っています。これは、 A1.7 の条件の $M,M^\prime$ から今度は $λx.M$ を考えた時、 $λx.M \rhd_{\alpha0} λx.M^\prime$ が成り立つのは明らかです。これを部分式として考えると $x,y$ が bound なので α-contraction の条件と重なることになります。