where 
, 
and 
is some weaker relation than
.
Lemmas in the library must be named opid-of-
_weakening_ index, where the _ index is optional,
and is only needed to distinguish lemmas if there is more than one for
a given 
.
Currently weakening lemmas are required for all reflexive relations
with 
being equality. They extend the usefulness of the
transitivity and functionality lemmas.