dest_forall : term -> term * term

SYNOPSIS: Breaks apart a universally quantified term into quantified variable and body.
DESCRIPTION: dest_forall is a term destructor for universal quantification: dest_forall `!var. t` returns (`var`,`t`).
FAILURE CONDITIONS: Fails with dest_forall if term is not a universal quantification.
SEE ALSO: is_forall, mk_forall, strip_forall.