(a) Frank's eta-expansion lemmas being very nice
(b) other rather reasonable means for understanding focusing existing such as NoamBobDan, and
(c) some of them just today falling over and not doing what I want them to
...I am still utterly enamored of these fiddly token-passing translations.
I think ultimately that Church encodings are their not-so-distant cousin. I have these on the brain lately because I am quite convinced that in a just world I should be able to read off what positives in HLF ought to do from what the negatives are already doing. Only a few technical hiccups throw that plan off the rails.
As it happens, the phenomenon of focusing itself seems to be the key idea that makes all of these translations (nicely) provably correct, because it brings down the level of nondeterminism with which your precious bundle of target-language connectives is decomposed to, ideally, none, and generally, something reasonable.
It's perhaps inexplicable, then, that I just cannot leave alone the idea of also viewing focusing merely as a fiddly token-passing encodable mode-of-use of ordinary linear logic, with a dash of first-order quantification, or else an ordered context, whichever you prefer.
I just half an hour ago noticed an awfully nice clean-up theorem that says effectively: the translation that translates differently on both sides of the turnstile doesn't really translate differently. They're (inductively) the same proposition up to the addition of a token consumer or producer. It's just not a shallow fact (except at the atoms, which I should have been looking to for advice the whole time!) but a deep inductive one.
So the punchline's the same, that cut elimination and identity proofs for full focused logic "just fall out" of cut and identity for linear logic, but it's epsilon closer to me really believing that it's simple.