Discussion of the basic idea of the Tait--Martin-Loef proof of confluence for untyped lambda calculus.  Let me know any requests for what to discuss in Chapter 8!