Applies a conversion to both arguments of a binary operator.
LIBRARY
DESCRIPTION
If c is a conversion that when applied to t1 returns the theorem
|- t1 = t1' and when applied to t2 returns the theorem
|- t2 = t2', then BINOP_CONV c (Term`f t1 t2`) will return the
theorem
|- f t1 t2 = f t1' t2'
FAILURE
BINOP_CONV c t will fail if t is not of the general form
f t1 t2, or if c fails when applied to either t1 or t2, or if c
fails to return theorems of the form |- t1 = t1' and |- t2 = t2'
when applied to those arguments. (The latter case would imply that
c wasn’t a conversion at all.)