lambda conversion,
n. the rule,
in particular, λ x[x](a) = a, and λ x[y](a) = y.
λ x [Fx] (a) = F(a)
for the application of the lambda operator, λ; that is, the application to a of the abstracted predicate ... is an x such that Fx, is equivalent to Fa. More generally,
λx[... x...](a) = ... a... ;
in particular, λ x[x](a) = a, and λ x[y](a) = y.