RESORT_FORALL_CONVConv.RESORT_FORALL_CONV : (term list -> term list) -> convReorders bound variables under universal quantifiers.
A call to RESORT_FORALL_CONV f t strips the outer
universally-quantified variables of t, giving a list
vs, such that t is of the form
!vs. body. The list vs is then passed to the
function argument f. The result of the call
f vs is expected to be a new list of variables
vs', and the result of the conversion is the theorem
|- (!vs. body) <=> (!vs'. body)The function f is generally expected to return a
permutation of the variables appearing in the term vs, but
may in fact introduce fresh variables that are fresh for
body, and may also remove variables from vs
that also don’t appear in body.
Given a term t, fails if t is not of
boolean type. Fails if when applied to the outermost universally
quantified variables (permitted to be the empty list) the function
f returns a list of terms that are not all variables. Also
fails if either f returns a list that does not include
variables from vs that appear in the body of
t, or if it includes variables that are in the body, but
which were not originally bound.