ML two objects of type term are equal if and only if they are
--convertible variants of each other. That is, they are equal if and
only if the
bound variables can be renamed so that the terms are identical. For objects
of type proof, rule and declaration, two objects are equal
if and only if they are the same object.