\chapter{Existential Quantifiers}
\section{Ex}\label{feih}Let $ \alpha $ be a type.
\begin{definition}\label{def:fgih}
We define $\mname{ex}$ to be ${\uniddcgcg Q : {{\alpha}\unicdbdjdcd{o}} .  {\unicdcdadad P : {o} .  {{({\unicdcdadad x : {\alpha} .  {{{Q}~{x}}\unicdbdjdcd{P}}})}\unicdbdjdcd{P}}}}$ of type ${{({{\alpha}\unicdbdjdcd{o}})}\unicdbdjdcd{o}}$.
\end{definition}
Since Proofgold has no polymorphism there is no single
object corresponding to existential quantification.
Instead there is a constructor ${\mname{Ex}}$
that takes a type argument and is always expanded away 
using the definition above
as part of normalization.

\section{Notation for Existential Quantifiers} % Ex
{\bf{Notation.}} We use $\bindfgihjgdhehdh x,\ldots,y  . $ as a binder notation corresponding to a term constructed using ${\mname{ex}}$.

