----------------------------------------------------------------------
mk_exists                                                 (boolSyntax)
----------------------------------------------------------------------
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.

----------------------------------------------------------------------