Finished revising that intuitionistic letcc paper, submitted it again. Never going to be totally satisfied with that business, but at least it's formalized.
At D's I sketched the diagram from here for marymcglo. I think she appreciated it.
Re: unification: After days of hoping some successful alternative to the broken pile of inductive invariants would magically pop into my head, at least some candidate alternative did magically pop into my head as soon as I got home. The thing I hadn't considered before choosing how to quantify over instantiations of evars independently for evars appearing in terms and types ~ if this idea works out, it would explain perfectly why I've been struggling with invariants that always seem wrong at one end or the other of the proof.