strip_res_exists : (term -> ((term # term) list # term))
STRUCTURE
SYNOPSIS
Iteratively breaks apart a restricted existentially quantified term.
DESCRIPTION
strip_res_exists is an iterative term destructor for restricted existential quantifications. It iteratively breaks apart a restricted existentially quantified term into a list of pairs which are the restricted quantified variables and predicates and the body.
   strip_res_exists "?x1::P1. ... ?xn::Pn. t"
returns ([("x1","P1");...;("xn","Pn")],"t").
FAILURE
Never fails.
SEEALSO
HOL  Trindemossen-1