There are many proofs use induction or recursion on $\omega$, or on an arbitary (may be uncountable) ordinal. Are there some good examples of proofs which use a big but computable ordinal?
The original proof of Ramsey theorem and Hales-Jewett theorem use induction on $\omega^2$, but the using is not essential, because Erdos and Shelah have given better bounds by using induction just on $\omega$. And further more $\omega^2$ shouldn't be considered big.
A typical use of big ordinal induction is proving the consistence of axiom systems, for example, using $\varepsilon_0$-induction to prove the consistence of PA. This is one kind of examples.
The existence of Goodstein function uses the induction on $\varepsilon_0$, and I think it's just a directly explaining of how do recursion on ordinal works.
Are there more examples?