dest_pforall : term -> term * term
STRUCTURE
LIBRARY
pair
SYNOPSIS
Breaks apart paired universal quantifiers into the bound pair and the body.
DESCRIPTION
dest_pforall is a term destructor for paired universal quantification. The application of dest_pforall to "!pair. t" returns ("pair","t").
FAILURE
Fails with dest_pforall if term is not a paired universal quantification.
SEEALSO
HOL  Trindemossen-1