Applies a conversion to both arguments of a binary operator.
DESCRIPTION
If c is a conversion where c `l` returns |- l = l' and c `r` returns
|- r = r', then BINOP_CONV c `op l r` returns |- op l r = op l' r'. The
term op is arbitrary, but is often a constant such as addition or
conjunction.
FAILURE CONDITIONS
Never fails when applied to the conversion. But may fail when applied to the
term if one of the core conversions fails or returns an inappropriate theorem
on the subterms.