Nice post! By the way, I'd love to see a readable/beginner's introduction to dealing with worlds in Twelf. I've read the Twelf wiki a few times, and also Harper/Licata's Mechanizing Metatheory in a Logical Framework, which are quite good—but a gentle introduction would be really nice too.