simrob and I were talking a bit about the cut elim proof in that unpublished "A Constructive Approach to the Resource Semantics of Substructural Logics" paper Frank and I wrote some time ago. I twelfed it up and found that I had in fact neglected to make the induction hypothesis as strong as it really should have been: J should include right focus on some positive prop B as well as left focus and right inversion as it already does.Last night managed to hang out with Dannel, and before that failed again to hang out with
gustavolacerda. Much like I keep failing to hang out with skamille. Post-college socialization in a large metropolitan area is so complicated, man. Anyway there's the holiday party tomorrow. 