Theorem: The composition of group homomorphims is a homomorphism.
This example illustrates that beta reduction works well with paramodulation.
The composition of two functions f and g is expressed as the lambda term lambda(x,f(g(x))). The verification that the composition of homomorphisms is a homomorphism is a straightforward piece of equational reasoning. However, we also need to prove that if Phi maps G to H and Psi maps H to K then the composition maps G to K. In this file, the groups G, H, and K are given by "propositional functions", that is, G, H, and K are treated as constants, and "x belongs to G" is represented by Ap(G,x) = $T. ($T means "true").
This theorem illustrates how lambda logic can sometimes make it very easy to formulate a precise version of a theorem that is rather difficult to formulate in set theory or in a first-order algebraic theory. Wick and McCune  showed how to formulate and prove this theorem in set theory. It was quite difficult.
 Wick, C., and McCune, W., Automated reasoning about elementary point-set topology, J. Automated Reasoning 5(2) 239-255, 1989.