I see this as a general problem in higher dimensional algebra, that there will need to be "higher dimensional rewriting". John Baez has illustrated the higher dimensional thinking by displaying the picture

$$||| \;\; ||| ||$$ $$||| \;\; |||||$$

which is easily seen to illustrate $2 \times (3+5)= 2 \times 3 + 2 \times 5$ but the 1-dimensional formula involves various conventions, and is less transparent. We have found diagrammatic rewriting useful in dealing with rotations in double groupoids (with connections), and there is a 3-dimensional rewriting argument in Section 5 of

F.-A. Al-Agl, R. Brown, R. Steiner, `Multiple categories: the equivalence between a globular and cubical approach', Advances in Mathematics, 170 (2002) 71-118.

which proves a key braid relation (Theorem 5.2).

So there is the interesting question of how to cope say with a 5-dimensional rewrite? Maybe computers could handle it?

These situations could well occur in algebras with partial operations whose domains are defined by geometric conditions, and with strict axioms.