Easy lambda-terms are not always simple (Q2889181)

A closed lambda term \(M\) is said to be easy if, for any other closed term \(N\), the lambda theory generated by \(M = N\) is consistent. Simple easiness has a rather technical definition. Roughly, as the authors say, \(M\) is simply easy if, for every lambda term \(N\), there is an easy intersection type system which generates a filter model satisfying \(M = N\). Simple easiness, known to imply easiness, also allows the proof of consistency results. This paper solves Problem 19 of the TLCA list in proving that easiness does not imply simple easiness. In fact, the authors provide a non-empty co-r.e. set of easy, but not simply easy, lambda terms.