Injectivity not required for unification algorithms? When learning about a general unification algorithm, we learned the rule decompose, which states unifying

$$G \cup \{f(a_0,...a_k)=f(b_0,...,b_k)\} \Rightarrow G \cup \{a_0=b_0,...a_k=b_k\}.$$

The question of, "What if $f$ is not injective?" stood out to me. Say $f$ is not injective, and we traverse that branch of computation where $f(a_0,...a_k)=f(b_0,...,b_k) \Rightarrow \{a_0=b_0,...,a_k=b_k\}$ and lead to failure. Is it possible that there's another way to assign $a_0,...,a_k$ to $b_0,...b_k$ such that it's unifiable?  

I was thinking maybe of an example to demonstrate what I mean. This may not be a good example, but say we consider $f(x,y) = x+y$, and we want to unify $f(h(a),g(b)) = f(g(c),h(d))$ then we would fail by assigning $\{h(a) = g(c), g(b)=h(d)\}$ by decompose, but succeed in unification if instead we first switch the arguments of $f$ (valid since $f(a,b)=f(b,a)$), which will yield $\{a \mapsto d, b \mapsto c\}$.

I was reading a bit about it in this paper on page 6 where they discuss the idea of strictness in terms of decompose, but I don't quite understand it, and more generally how we can perform this unification step of decompose on a general $f$ without somehow backtracking on failure.
Here $f$ is not a mathematical function.  Rather, it is a function symbol.  Don't think of $f(a,b)$ as the result of evaluating the function at parameters $a,b$.  Rather, think of it as a term in a symbolic expression -- it is a syntactic object that is not intended to be interpreted in the way you are interpreting it.

If you like, you can think of it as though every function symbol in a symbolic expression is an injective function; but that's not really accurate, that's just a crude way to think about symbolic expressions.

You can't define $f(x)=x+y$.  $f$ is an uninterpreted function symbol.  You're not allowed to define a particular function.  Rather, $f$ is a stand-in for a function that is not yet defined. One way to think about it is that any conclusions that you draw from unification, are conclusions that should hold for all functions $f$ (not just a single one).