dest_forall : term -> term * term
STRUCTURE
SYNOPSIS
Breaks apart a universally quantified term into quantified variable and body.
DESCRIPTION
If M has the form !x. t, then dest_forall M returns (x,t).
FAILURE
Fails if M is not a universal quantification.
SEEALSO
HOL  Trindemossen-1