Got a bunch of positive progress hacking on this proof. I think I've very nearly reached bottom and found the right things to prove directly from the formulation of the system. Somehow it's awfully hard to just show that if you substitute M for a variable with a strict occurrence and the result is well-typed, then M has the type of the variable. This being precisely what I need to avoid the spurious extra ex post facto check that lead to that nasty infinite loop.
Had dinner at Kazansky's with madmadammim and phoebus. The waitress was all apologetic that they were out of hamburger buns but my burger tasted really good on the sourdough they substituted. The conversation was largely lingustic wankery. So much fun.
Sabrina came over for adam's showing of Enterprise. I think I'm missing out on a lot by only watching the occasional episode when I happen to be around for it, but they're still entertaining. VASE IN THE FACE!