Here is a different (more direct) presentation of the argument for Fact 2; the algorithm in the previous proof can be extracted from here as well:
Proof: We proceed by induction on the length of the proof to show that for all whenever a string has a proof from of length at most then it has a proof of the required form.
This is clear if Suppose has a proof of length and the result holds for all proofs of length at most If is an axiom, it has a proof of length If in is the result of applying the extension rule to some then has (by the induction hypothesis) a proof of the required form, and is a proof of of the required form.
Finally, suppose that in is the result of applying compression to and By the induction hypothesis, and have proofs and respectively, of the required form. If in the extension rule is used, then it must in particular be used at the last step, so appears in Restricting to its initial segment that ends in gives us a proof of of the required form. Similarly with
We can then assume that extension is neither used in nor in So, for where consists of applications of the axioms rule, and consists of applications of compression. Then is a proof of of the required form.