The tool does not recognize `λn. n` as eta-equivalent to the Church 1 (`λfn. f n`).

This might prevent it from recognizing `E := λmn. n m` as a solution to the exponentiation problem. (I can't check it right now). But it certainly does not help when testing.