Applies a conversion to the right-hand argument of an equality.
DESCRIPTION
If c is a conversion that maps a term t2 to the theorem |- t2 = t2',
then the conversion RHS_CONV c maps applications of the form t1 = t2 to
theorems of the form:
|- (t1 = t2) = (t1 = t2')
FAILURE
RHS_CONV c tm fails if tm is not an an equality t1 = t2,
or if tm has this form
but the conversion c fails when applied to the term t2. The
function returned by RHS_CONV c may also fail if the ML function
c:term->thm is not, in fact, a conversion (i.e. a function that maps
a term t to a theorem |- t = t').