Definition of the Mendler encoding

We consider using Mendler's technique of abstracting out problematic types with new type variables, and how this can yield a lambda encoding where the programmer is in charge of when to make recursive calls (rather than in the Church encoding, where the data present the programmer's combining function with the results of all possible recursive calls on immediate subdata).