Wrote some eta-expansion code. Discovered that I can't expand all eta-contracts without going to much greater effort, but I think the version I coded will be enough to cover the amount by which twelf falls short of maintaining eta-longness itself.

Hung out with Drew Hoskins a bit today, had some dinner at Uncle Sam's with him. He was an undergrad in the same class as me at CMU. I hadn't seen him for a couple years. He's been working at Microsoft in the compilers group, apparently, having fun there, keeping busy. His occasion for being in pittsburgh is some sort of national bridge tournament.