Applies two conversions to the two sides of an application.
DESCRIPTION
If c1 and c2 are conversions such that c1 `f` returns |- f = f' and
c2 `x` returns |- x = x', then COMB2_CONV c1 c2 `f x` returns
|- f x = f' x'. That is, the conversions c1 and c2 are applied
respectively to the two immediate subterms.
FAILURE CONDITIONS
Never fails when applied to the initial conversions. On application to the term,
it fails if either c1 or c2 does, or if either returns a theorem that is of
the wrong form.
COMMENTS
The special case when the two conversions are the same is more briefly achieved
using COMB_CONV.