LAST_EXISTS_CONV : conv -> conv
STRUCTURE
Conv
SYNOPSIS
Applies a conversion to the last existential quantifier (and its body) in a chain.
DESCRIPTION
Application of LAST_EXISTS_CONV c to the term ``?x1 .. xn x. body`` will apply c to the term ``?x. body``. If the result of this application is the theorem |- (?x. body) = t, then the result of the whole will be 
   |- (?x1 .. xn x. body) = (?x1 .. xn. t)
FAILURE
Fails if the term is not existentially quantified, or if the conversion c fails when it is applied.
SEEALSO
BINDER_CONV, LAST_FORALL_CONV, STRIP_QUANT_CONV
HOL  Kananaskis-13