is equivalent to the following formula: $$\mu = \forall x \forall y \bigwedge_{\sigma, \tau \in \Sigma}\Big( \sigma(x) \wedge \tau(y) \rightarrow \gamma_{\sigma, \tau}(x,y)\Big)$$ To see this, let us consider a model ${\ensuremath{\mathfrak{A}}}$ of $\chi$. For all elements $a, b$ of ${\ensuremath{\mathfrak{A}}}$ of types $\sigma$, $\tau$, respectively, one of the disjuncts has to be satisfied. Since each element satisfies exactly one unary type, the disjunct $\sigma(x) \wedge \tau(y) \wedge \gamma_{\sigma, \tau}(x,y)$ is satisfied and therefore also $\mu$ is satisfied.

Now, consider a model ${\ensuremath{\mathfrak{A}}}$ of $\mu$. Then for all elements $a, b$ of ${\ensuremath{\mathfrak{A}}}$ the conjunction is satisfied. In particular the conjunct $\sigma(x) \wedge \tau(y) \rightarrow \gamma_{\sigma, \tau}(x,y)$ is satisfied, where $\sigma$ and $\tau$ are the types of $a$ and $b$, respectively. Therefore also $\sigma(x) \wedge \tau(y) \wedge \gamma_{\sigma, \tau}(x,y)$ and hence $\chi$ are satisfied.

The formula $\mu$ can be easily translated into a set of universal constraints $C_\forall$. For all unary types $\sigma$ and $\tau$, the set $C_\forall$ contains a constraint $(\sigma, \gamma, \tau)$ for each binary type $\gamma$ that is not consistent with $\gamma_{\sigma, \tau}(x,y)$. Next we show how to translate the second part of $\xi$ into existential constraints. As before, we translate $\psi_i$ into the disjunctive normal form $\bigvee_{\sigma, 