A closed lambda term is easy if adjoining to the equations of beta equivalence remains nontrivial for every closed lambda term . If is easy, then is easy for every closed : use the consistent equation to obtain . Since is not easy and solvability produces by applications, easy terms are unsolvable. The converse need not hold.
New to topics? Read the docs here!