**Metamath**

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.