Research stuff is awfully frustrating today. I've gone through the metatheory of LF and LF-like systems a million times and there are still important things about it I deeply don't understand. I had thought that somewhere in the structure of the proofs there was something that determined to some extent what the definition of context validity (and in the same sense type-well-formedness) had to be, but I seem to have the proofs of substitution and identity going through in a certain style that work syntactically as long as everything is simply-typed. Somehow this seems inevitable, since if you added a few new trivial modes of truth that behaved exactly like truth but were marked syntactically differently, the system couldn't "know" that this was wrong.
And at some level I think this is precisely the same problem with the old linear-dependency stuff ~ it was impossible to tell what should be done at the type level, because there were not sufficient theorems that we knew had to be true to tell us when we had got the definitions right. At the term level, substitution and identity are great tools, but at the type level, what?