Invertible lambda term
= Invertible lambda term
{title2=$p\bullet q=_{\beta\eta}I=q\bullet p$}
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.