In higher order logic, one sometimes defines the existential quantifier by $$(\exists x. \phi(x)) := (\forall \rho.(\forall x.\phi(x)\to\rho)\to\rho).$$ I am having trouble proving that $$(\exists x.\exists y.\psi(x,y)) \to (\exists y.\exists x.\psi(x,y)).$$
Is this even true? If not, what would be a counter example?
The trick is to unfold and instantiate both instances of $\exists$ in the hypothesis with the right hand side as follows:
Let $\rho_0 := \exists y.\exists x.\psi(x,y)$, then the following is a derivation tree (read from bottom to top):
\begin{align*} (\exists x.\exists y.\psi(x,y))&\vdash \rho_0\\ ((\forall x.(\exists y.\psi(x,y)) \to \rho_0)\to \rho_0) &\vdash \rho_0\\ &\vdash(\forall x.(\exists y.\psi(x,y)) \to \rho_0)\\ &\vdash_x (\exists y.\psi(x,y))\to\rho_0\\ \exists y.\psi(x,y)&\vdash_x\rho_0\\ (\forall y.(\psi(x,y) \to\rho_0)\to\rho_0)&\vdash_x \rho_0\\ &\vdash_x \forall y.(\psi(x,y)\to\rho_0)\\ &\vdash_{x,y}\psi(x,y) \to(\exists y.\exists x.\psi(x,y))\\ \psi(x,y)&\vdash_{x,y}\psi(x,y), \end{align*}
Where the last step follows from the general observation that (again, from bottom to top) \begin{align*} \phi(x)&\vdash_{x}\exists x.\phi(x)\\ \phi(x),(\forall x.\phi(x)\to\rho) &\vdash_{x,\rho} \rho\\ \phi(x),\phi(x)\to\rho &\vdash_{x,\rho}\rho\\ \rho&\vdash_\rho\rho. \end{align*}