dest_pforall : term -> term * term
STRUCTURE
pairSyntax
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
dest_forall
,
is_pforall
,
strip_pforall
HOL
Trindemossen-1