RES_SELECT_CONV : conv
STRUCTURE
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
HOL  Kananaskis-13