12 The word "boost" there was basically useless.

The basic idea is to prove cut admissibility and identity expansion for the focused system only, and then use that to prove the critical "boost" unfocused proofs admissibility" lemmas, which show that any unfocused inference is valid over to focused onesproofs. One reason that I like this presentation is that it shows how the completeness of focusing is a straightforward consequence of cut admissibility and identity expansion for the focused sequent calculus.

11 no reason not to tidy up once it's gone community wiki

{A \in \Gamma \quad qquad \Gamma \vdash A > P \over \Gamma \vdash P}{\it focus}

Proof: Straightforward induction on focused proofs (+ weakening for the unfocused proofs). QED.

10 put the alpha subscript in the right place(s)
{\Gamma, A \Rightarrow B \over \Gamma \Rightarrow A \supset B}{{\supset}R^\alphaB}{{\supset}R}{\Gamma \Rightarrow A(\alpha) \over \Gamma \Rightarrow \forall x.A(x)}{{\forall}Rx.A(x)}{{\forall}R^\alpha}

Case 4: (${\forall}R$, ${\forall}R^\alpha$, omitted)

9 tidy up \supset R - didn't have a superscript alpha in the unfocused calculus; [made Community Wiki]
8 expand on proof of Theorem 2