Transitivity lemmas give transitivity information for rewrite relations. They are used to construct the tactic justification in the ANDTHENC conversional.
Transitivity lemmas should be of form:
where 
and 
. For now there is a
restriction that 
should be the weaker of 
and 
.
ANDTHENC finds transitivity lemmas in the library by
assuming that a naming convention has been followed.
The lemmas must be named opid-of-
_transitivity_ index, where the _ index is
optional, and is only needed to distinguish lemmas if there is more
than one for a given 
. A transitivity lemma is not needed for
equality.