I've come across it multiple times now in proof theory papers that authors use (sometimes quite elaborate) inductions in order to prove easy results. The most striking example is the following, where O is the class of countable ordinals:
From: Jean H. Gallier, "What's so special about Kruskal's theorem and the ordinal $Γ_0$?", Annals of Pure and Applied Logic, 1991, p. 218.
It seems to me that this is a total overkill. In the paper we already know that O is well- and thus linearly ordered, so if we assume that $\alpha\not\leq \beta$, thus $\beta < \alpha$, then the antecedent gives us $\beta < \beta$, a contradiction.
Is the reason not to use such arguments that they are not constructive? But that would be odd, since the author's proof that transfinite induction is valid in his system of ordinals was itself non-constructive...