Applies a conversion to the left-hand argument of a binary operator.
DESCRIPTION
If c is a conversion that maps a term t1 to the theorem |- t1 = t1',
then the conversion LAND_CONV c maps applications of the form f t1 t2 to
theorems of the form:
|- f t1 t2 = f t1' t2
FAILURE
LAND_CONV c tm fails if tm is not an application where the rator
of the application is in turn another application, as f t1 t2,
or if tm has this form but the conversion c
fails when applied to the term t1. The
function returned by LAND_CONV c may also fail if the ML function
c:term->thm is not, in fact, a conversion (i.e. a function that maps
a term t to a theorem |- t = t').