mk_res_exists : ((term # term # term) -> term)
STRUCTURE
SYNOPSIS
Term constructor for restricted existential quantification.
DESCRIPTION
mk_res_exists("var","P","t") returns "?var :: P . t".
FAILURE
Fails with mk_res_exists if the first term is not a variable or if P and t are not of type ":bool".
SEEALSO
HOL  Kananaskis-13