dest_pforall
pairSyntax.dest_pforall : term -> term * term
Breaks apart paired universal quantifiers into the bound pair and the body.
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.
See also
boolSyntax.dest_forall,
pairSyntax.is_pforall,
pairSyntax.strip_pforall