 with \(A_D(\vec{x},\vec{y})\) being quantifier free. Thus \(A^D\) is not a formula of \({T}\) but of its augmentation via quantifiers \(\forall x^{\tau}\) and \(\exists y^{\tau}\) for all types \(\tau\). The translation proceeds by induction on the buildup of A. The cases where the outermost logical symbol of A is among \(\land\), \(\lor\), \(\exists x\), \(\forall x\) are rather straightforward. The crucial case occurs when A is an implication \(B\to C\). To increase readability we shall suppress the typing of variables. Let \(B^D\equiv \exists \vec{x}\, \forall \vec{y}\, B_D(\vec{x},\vec{y})\) and \(C^D\equiv {\exists \vec{u}\, \forall \vec{v}\, C_D(\vec{u},\vec{v})}\). Then one uses a series of judicious equivalences to bring the quantifiers in \(B^D\to C^D\) to the front and finally employs skolemization of existential variables as follows: 