I am having the hardest time finishing off this one system for the multilanguage paper. Every time I think I've finally got it done, I realize that I should've arranged something differently, or I need another nontrivial lemma to establish that something holds, or my induction doesn't really work, or whatever. And by the time I'm done, the goal is to make it look obvious enough that people's eyes will glide right over it without even having to pause. I'm beginning to fully appreciate Pierce's quote about how the proofs are almost always boring if the definitions are correct, but the definitions are almost always incorrect.