dest_res_exists : (term -> (term # term # term))
STRUCTURE
SYNOPSIS
Breaks apart a restricted existentially quantified term into the quantified variable, predicate and body.
DESCRIPTION
dest_res_exists is a term destructor for restricted existential quantification:
   dest_res_exists "?var::P. t"
returns ("var","P","t").
FAILURE
Fails with dest_res_exists if the term is not a restricted existential quantification.
SEEALSO
HOL  Kananaskis-10