RES_EXISTS_CONV : conv
STRUCTURE
res_quanLib
SYNOPSIS
Converts a restricted existential quantification to a conjunction.
DESCRIPTION
When applied to a term of the form ?x::P. Q[x], the conversion RES_EXISTS_CONV returns the theorem: 
   |- ?x::P. Q[x] = (?x. x IN P /\ Q[x])
which is the underlying semantic representation of the restricted existential quantification.
FAILURE
Fails if applied to a term not of the form ?x::P. Q.
SEEALSO
RES_FORALL_CONV, RESQ_EXISTS_TAC
HOL  Kananaskis-14