----------------------------------------------------------------------
RES_SELECT_CONV                                          (res_quanLib)
----------------------------------------------------------------------
RES_SELECT_CONV : conv

SYNOPSIS
Converts a restricted choice quantification to a conjunction.

KEYWORDS
conversion, restricted quantifier.

DESCRIBE
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_quanLib.RES_FORALL_CONV, res_quanLib.RES_EXISTS_CONV.

----------------------------------------------------------------------