One striking example that comes to mind is Nathan Jacobson's proof that rings satisfying the identity X^m = X are commutative. This is model-theoretic and proceeds by a certain type of factorization which reduces the problem to the (subdirectly) irreducible factors of the variety. These turn out to be certain finite fields, which are commutative, as desired. By (Birkhoff) completeness there must also exist a purely equational proof (in the language of rings) but even for small m this is notoriously difficult, e.g. m = 3 is often posed as a difficult exercise [1]. It's only recently that such a general non-model-theoretic proof was discovered by John Lawrence (as Stan Burris informed me). I don't know if it has been published yet, but see their earlier work [2].

So here, by "higher-order" conceptual structural reasoning, one is able to escape the confines of first-order equational logic and give a more conceptual proof than the brute-force equational proofs - arguments so devoid of intuition that they may have been discovered by an automatic theorem prover.

[1] http://groups-beta.google.com/group/sci.math/msg/9b884af731351f10

[2] S. Burris and J. Lawrence, Term rewrite rules for finite fields.
International J. Algebra and Computation 1 (1991), 353-369. http://www.math.uwaterloo.ca/~snburris/htdocs/MYWORKS/PAPERS/fields3.pdf

One striking example that comes to mind is Nathan Jacobson's proof that rings satisfying the identity $X^m = X$ are commutative. This is model-theoretic and proceeds by a certain type of factorization which reduces the problem to the (subdirectly) irreducible factors of the variety. These turn out to be certain finite fields, which are commutative, as desired. By (Birkhoff) completeness there must also exist a purely equational proof (in the language of rings) but even for small $m$ this is notoriously difficult, e.g. $m = 3$ is often posed as a difficult [exercise] 0. It's only recently that such a general non-model-theoretic equational proof was discovered by John Lawrence (as Stan Burris informed me). I don't know if it has been published yet, but see their earlier [work [1]] 1

So here, by "higher-order" conceptual structural reasoning, one is able to escape the confines of first-order equational logic and give a more conceptual proof than the brute-force equational proofs - arguments so devoid of intuition that they can been discovered by an automatic theorem prover.

1 S. Burris and J. Lawrence, Term rewrite rules for finite fields.
International J. Algebra and Computation 1 (1991), 353-369. http://www.math.uwaterloo.ca/~snburris/htdocs/MYWORKS/PAPERS/fields3.pdf