In this problem session I present a simple-looking problem of implementing formalisation involving higher-order terms (or more simply, terms with binders). Our existing tools and techniques are usually good enough to handle most of the practical cases for a simpler (in terms of implementation) system, but there are always exceptions…