 The three rules of inference listed in the previous section governing equality have nothing to do with the \(\lambda\)-calculus. The following lists rules of inference that relate the undefined notion of equality and the two term-building operations of the \(\lambda\)-calculus, application and abstraction.