It would be nice if other equations could be used as
identities in simplifying or manipulating equations.
This would, for instance, let me enter some identities
of my own that are useful in a particular setting and
use them as if they were real identities. This is
particularly useful when trying to reduce an equation