A key property of existential quantification (intuitionistic logic axiom
ax-ie2). (Contributed by Jim Kingdon, 31-Dec-2017.)
\( \vdash \forall x \, (\psi \rightarrow \forall x \, \psi) \rightarrow (\forall x \, (\varphi \rightarrow \psi) \leftrightarrow \exists x \, \varphi \rightarrow \psi) \)
\( \vdash \Finv x \, \psi \leftrightarrow \forall x \, (\psi \rightarrow \forall x \, \psi) \)
\( \vdash \Finv x \, \psi \rightarrow (\forall x \, (\varphi \rightarrow \psi) \leftrightarrow \exists x \, \varphi \rightarrow \psi) \)