\DOC mk_exists

\TYPE {mk_exists : term * term -> term}

\SYNOPSIS
Term constructor for existential quantification.

\DESCRIBE
If {v} is a variable and {t} is a term of type {bool}, then
{mk_exists (v,t)} returns the term {?v. t}.

\FAILURE
Fails if {v} is not a variable or if {t} is not of type {bool}.

\SEEALSO
boolSyntax.dest_exists, boolSyntax.is_exists, boolSyntax.list_mk_exists, boolSyntax.strip_exists.
\ENDDOC