I updated the text that it becomes clearer - Church did not make a difference between the lambda calculus as a term language and his Hilbert system. Since LC by itself is already pretty useful, the two were disentangled at some point.

To my knowledge, System T has product types but simply typed lambda calculus does not (at least according to Church: "A Formulation of the Simple Theory of Types" and Benzmüller, Miller: "Automation of Higher-Order Logic", which are my standard sources regarding STT).

By the way, thanks for the link - I was aware that in higher order logic, ∀X.X→X subsumes the cut rule but I forgot that you can use it as an axiom scheme in first order logic as well.

It seems we have different notions of usual because I assume explicit contraction rules by default :-) If you use a sequent calculus with built-in contraction, there is still a linear proof of the formula with n applications of w:r,∀:r,... . The sequent size never grows beyond two formulas as well. Could you perhaps clarify what the "number of bits" measures?

Reading on further, I'm not even sure if you speak about proof checking or the sizes of the actual proofs :(

I would also be surprised if the non-elementary speedup of a sequent calculus with cut against one without cut can be remedied by picking the right axiom system. So I'm not even sure about the "typical proof systems are equivalent up to a polynomial factor." If I remember correctly, proof systems are often incomparable when it comes to proof complexity in the sense that there are formulas F and G such that proof system A has a short proof of F and a long proof of G but a proof system B has a short proof of G and a long proof of F.

I'm still trying to understand the actual question, but I'm wondering why a sequent calculus proof of ∀x1...∀xn 0=0 should be quadratic in the formula size. It should be n applications of ∀:r inferred from 0=0 as an instance of the reflexivity axiom of equality.