 Proof sketch: The idea is the following: Let φ(x) be a formula, like above, for which φ(m) does not have a short proof in Sn for any m. Suppose we have a higher type system Sn+1 in which we can prove ∀xφ(x). This proof is of constant length. Thus each φ(m) is derivable from this universal statement by one application of the logical rule ∀xφ(x) → φ(t). Thus φ(m) has in that system for all m a short proof.