THEN_CONSEQ_CONV cc1 cc2 corresponds to c1 THENC c2 for
classical conversions. Thus, if cc1 returns |- t' ==> t when
applied to t, and cc2 returns |- t'' ==> t' when applied to
t', then (THEN_CONSEQ_CONV cc1 cc2) t returns |- t'' ==> t.
THEN_CONSEQ_CONV can handle weakening as well: If cc1 returns
|- t ==> t' when applied to t, and cc2 returns |- t' ==> t''
when applied to t', then (THEN_CONSEQ_CONV cc1 cc2) t returns
|- t ==> t''. Finally, if cc1 returns |- t = t' when applied to t,
and cc2 returns |- t' = t'' when applied to t', then
(THEN_CONSEQ_CONV cc1 cc2) t returns |- t = t''. If one of the
conversions returns an equation, while the other returns an
implication, the needed implication is automatically deduced.