dest_res_forall : term -> (term # term # term)
STRUCTURE
res_quanLib
SYNOPSIS
Breaks apart a restricted universally quantified term into the quantified variable, predicate and body.
DESCRIPTION
dest_res_forall is a term destructor for restricted universal quantification: 
   dest_res_forall "!var::P. t"
returns ("var","P","t").
FAILURE
Fails with dest_res_forall if the term is not a restricted universal quantification.
SEEALSO
mk_res_forall, is_res_forall, strip_res_forall
HOL  Trindemossen-1