simrob's draft paper and accompanying formalization reminds me that I don't know of anything stopping me from fully twelfing up my own completeness-of-focusing proof, which ought to run fairly closely parallel to his. If I remember right, the places where he gets a for-free uniform substitution principle of focal things into suspended things, e.g.Γ |- [P]
Γ, <P> |- C
-------------------------
Γ |- C
I expect I should also get that for free from the cut principle for the unfocused logic, because the translation of [P] on the right and <P> on the left should work out to the same thing.
Hmm I should try doing that one of these days...
