I believe that the formulation of lambda I was wondering about yesterday is:
$d y A $.
df-lambda $a |- ( lambda x A ) = { <. x , y >. | y = A } $.
This lets me prove such things as ( ( lambda x x ) ` y ) = y. I'm probably not at the full power of the lambda calculus, though, because here "y" is required to be a set, while a lambda term is a class. So it's not clear I can apply this lambda term to itself.
School
Tomorrow is Alan's first day of 1st grade. It promises to be exciting.