\tau \in \Sigma}\big(\sigma(x) \wedge \tau(y) \wedge \gamma_{\sigma, \tau}(x,y)\big)$. Sorting by $\sigma$ and moving the existential quantifier inwards as far as possible yields that every conjunct of the second part of $\psi$ can be written as follows: $$\chi_i = \forall x \bigvee_{\sigma\in \Sigma} \Big(\sigma(x) \wedge \exists y \bigvee_{\tau\in \Sigma}\big( \tau(y) \wedge \gamma_{\sigma, \tau}(x,y)\big)\Big)$$ Using a similar argument as above one can show that each $\chi_i$ is equivalent to a formula: $$\mu_i = \forall x \bigwedge_{\sigma\in \Sigma} \Big(\sigma(x) \rightarrow \exists y \bigvee_{\tau\in \Sigma}\big( \tau(y) \wedge \gamma_{\sigma, \tau}(x,y)\big)\Big)$$ The formulas $\mu_i$ can be easily translated into a set of existential constraints $C_\exists$. For all $i$ and all $\sigma$, the set $C_\exists$ contains an existential constraint $(\sigma, E)$ where $E$ contains all tuples $(\gamma, \tau)$ that are consistent with $\gamma_{\sigma, \tau}$ where $\tau$ is a unary type and $\gamma$ is a binary type.

Observe that the sets $C_\exists$ and $C_\forall$ can be computed in exponential time (where the exponential blow-up comes from using the types).

The following notion will be used frequently. If an element has a unary type $\sigma$ we also say that it is *$\sigma$-labeled*. Consider a constraint problem $C$ over $T$, a $T$-structure ${\ensuremath{\mathfrak{A}}}$, a $\sigma$-labeled element $a$ and an existential 