strip_res_forall is an iterative term destructor for restricted universal
quantifications. It iteratively breaks apart a restricted universally
quantified term into a list of pairs which are the restricted quantified
variables and predicates and the body.
strip_res_forall "!x1::P1. ... !xn::Pn. t"