 Termination proof of monoidal coherence

Orient associativity towards right association and unit maps towards deletion of unit symbols. A lexicographic measure consisting of the number of leaves and the sum of the sizes of left subtrees decreases at every step. All overlapping reductions have commuting completions: the essential cases are the pentagon identity for a monoidal category, the triangle identity for a monoidal category, and the derived left and right unit identities. Induction on the decreasing measure makes every normalization arrow equal, proving that every structural arrow is determined by its endpoints.