----------------------------------------------------------------------
dest_pforall                                              (pairSyntax)
----------------------------------------------------------------------
dest_pforall : term -> term * term

LIBRARY
pair

SYNOPSIS
Breaks apart paired universal quantifiers into the bound pair and the body.

DESCRIBE
{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
boolSyntax.dest_forall, pairSyntax.is_pforall,
pairSyntax.strip_pforall.

----------------------------------------------------------------------