This file simply verifies the standard fixed point construction of lambda calculus. If you are not familiar with this construction, it is explained in Lambda Calculus. There is a also a discussion of this example in Implicit and Explicit Typing in Lambda Logic.