res_quanLib.mk_res_exists

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

STRUCTURE: res_quanLib
SYNOPSIS: Term constructor for restricted unique existential quantification.
DESCRIPTION: 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: dest_res_exists_unique, is_res_exists_unique

HOL Kananaskis-13