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"