Easy lambda term
= Easy lambda term
A closed <lambda term> $E$ is easy if adjoining $E=M$ to the equations of <beta equivalence> remains nontrivial for every closed <lambda term> $M$. If $E$ is easy, then $ET$ is easy for every closed $T$: use the consistent equation $E=\lambda x.M$ to obtain $ET=M$. Since $I$ is not easy and solvability produces $I$ by applications, easy terms are unsolvable. The converse need not hold.