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