strip_pforall : term -> term list * term
STRUCTURE
pairSyntax
LIBRARY
pair
SYNOPSIS
Iteratively breaks apart paired universal quantifications.
DESCRIPTION
strip_pforall "!p1 ... pn. t"
returns
([p1,...,pn],t)
. Note that
strip_pforall(list_mk_pforall([p1,...,pn],t))
will not return
([p1,...,pn],t)
if
t
is a paired universal quantification.
FAILURE
Never fails.
SEEALSO
strip_forall
,
dest_pforall
HOL
Kananaskis-14