[Hendrikto]

I do not get why you mean by plus being injective.

`plus(1, 2, C). C = 3.`

`plus(0, 3, C). C = 3.`

Isn't that a counterexample, showing how it is not injective?

[mathetic]

Yes, I was thinking total with respect to _intuitive_ arguments, but wrote injective. Sorry.