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