 The syntactic identity relation \(\equiv\) is not part of the official syntax of \(\lambda\)-calculus; this relation between \(\lambda\)-terms belongs to the metatheory of \(\lambda\)-calculus. It is clearly a rather strict notion of equality between \(\lambda\)-terms. Thus, it is not the case (if \(x\) and \(y\) are distinct variables) that \(\lambda x[x] \equiv \lambda y[y]\), even though these two terms clearly ‘behave’ in the same way in the sense that both are expressions of the identity operation \(x \Rightarrow x\). Later we will develop formal theories of equality of \(\lambda\)-terms with the aim of capturing this intuitive equality of \(\lambda x[x]\) and \(\lambda y[y]\).