When Mathematica is pattern-matching expressions, does it use first order or second order unification.
Just to clarify the difference between first order and second order unification:
In Second order unification, it is possible to replace a pattern variable with a function: When the expression
Plus[3,3] is matched with the pattern
f, the matching succeeds and
f is bound to
Plus[#, #]& or