前回の記事の要約: (A): M →1β N, M ≡α M' ⇒ M' →1β N (B): M ▷1β N ⇒ [t/s]M →1β [t/s]N という二つの命題を証明しようとしたが(A)と(B)の証明が相互依存になってしまって、それを二つの証明の帰納法を同時に実行することで解消するという大掛かりな方法を…