Composition of lambda terms ($p\bullet q\equiv \lambda x.p(qx)$)

Choose $x$ fresh for the free variables of $p,q$. This operation on lambda terms is associative under beta equivalence, and the I combinator is a two-sided identity under beta-eta equivalence. The latter use of eta conversion is necessary in general.

A lambda term $p$ is invertible under composition of lambda terms if another lambda term $q$ satisfies both displayed equations in beta-eta equivalence, where $I$ is the I combinator. An inverse on just one side does not by itself justify using the inverse equation on the other side.