RESORT_EXISTS_CONV : (term list -> term list) -> conv
STRUCTURE
Conv
SYNOPSIS
Reorders bound variables under existential quantifiers.
DESCRIPTION
A call to RESORT_EXISTS_CONV f t strips the outer existentially-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.
FAILURE
Given a term t, fails if t is not of boolean type. Fails if when applied to the outermost existentially 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.
SEEALSO
RESORT_FORALL_CONV, sort_vars
HOL  Kananaskis-14