----------------------------------------------------------------------
mk_res_exists_unique                                     (res_quanLib)
----------------------------------------------------------------------
mk_res_exists_unique : (term # term # term) -> term

SYNOPSIS
Term constructor for restricted unique existential quantification.

DESCRIBE
{mk_res_exists_unique ("var","P","t")} returns {"?!var :: P . t"}.

FAILURE
Fails with {mk_res_exists_unique} if the first term is not a
variable or if {P} and {t} are not of type {":bool"}.

SEEALSO
res_quanLib.dest_res_exists_unique, res_quanLib.is_res_exists_unique.

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