COMB_CONVConv.COMB_CONV : conv -> convApplies a conversion to both immediate sub-terms of an application.
If t is an application term of the form
f x, and c is a conversion, such that
c maps f to |- f = f' and
x to |- x = x', then COMB_CONV c
maps t to |- f x = f' x'.
If one of the two sub-calls raises the UNCHANGED
exception, then the result of that call is taken to be the reflexive
theorem (|- x = x if c x raises the exception,
for example). If both conversions raise the UNCHANGED
exception, then so too does COMB_CONV c t.
COMB_CONV c t fails if t is not an
application term, or if c fails when applied to the rator
and rand of t, or if c is not in fact a
conversion (i.e., a function which maps terms t to a
theorem |- t = t').