Reference: Cancellability of the Dyck congruence I consider the Dyck congruence $\equiv$ on a parenthesis alphabet $\Sigma = \{a, \bar a, b, \bar b\}$, i.e. the least congruence on $\Sigma^*$ such that $a \bar a \equiv \varepsilon $ and $b \bar b \equiv \varepsilon$.

It appears that $\equiv$ can be cancelled, i.e. for every $v$, $w_1$, $w_2 \in \Sigma^*$, if $vw_1 \equiv vw_2$, then $w_1 \equiv w_2$ (and analogously for cancellation from the right).

Does someone know a literature reference for this property?  I wasn't able to find anything along those lines.
Your assertion is wrong, the congruence $\equiv$ is not cancellable from the right: for instance $\bar a a \bar a \equiv \bar a$, but $\bar a a \not\equiv 1$.

By the way the quotient $\Sigma^*/{\equiv}$ is not a group, but a monoid, called the polycyclic monoid, first introduced in [1].

[1] M. Nivat and J-F. Perrot, Une généralisation du monoïde bicyclique, Comptes Rendus de l'Academie des Sciences de Paris 271 (1970), 824-827.