Definition 1.17 から α-conversion の話なのだけれども、構成が解りずらかったので自分なりに整理します。

Lemma 1.15 と 1.16 が前段にあるのだけれども、(Lemma 1.15 は直後と 1.30 で、1.16 は ≡ と ≡α の関係で 1.20 で)どちらも後で再び出て来ます。

Example 1.18 を経て、 Lemma 1.19 が Lemma A1.5(≡α0について)を参照しつつ示されます。

Definition A1.6 では 1.17 を参照して α-contraction(s) を示します。 また 1.19 を示すには、 ≡α と ≡α0 の関係を示すことで明らかになるのだけれども Lemma A1.8 までを参照する必要があります。

A1.8 で α と α0 の関係が示されて、Lemma 1.20 以降へ話を進められると思ったのも束の間、 Lemma 1.21 では A1.10 を参照しています。 A1.10 では更に CF58 も参照しています。

CF58 については 1.17 の説明で p.91、 1.20 の証明で p.95、A1.10 の証明で、p.95,96-103 等、頻繁に参照されています。