Record that one equivalence relation refines another

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.

Example: (defthm bag-equal-refines-set-equal (implies (bag-equal x y) (set-equal y x)) :rule-classes :refinement)

Also see defrefinement.

General Form: (implies (equiv1 x y) (equiv2 x y))

`rewrite` rules may be
used while trying to maintain

The macro form `defthm` of rule-class

Suppose we have the `rewrite` rule

(bag-equal (append a b) (append b a))

which states that `append` is commutative modulo bag-equality.
Suppose further we have established that bag-equality refines set-equality.
Then when we are simplifying `append` expressions while maintaining
set-equality we use `append`'s commutativity property, even though it
was proved for bag-equality.

Equality is known to be a refinement of all equivalence relations. The
transitive closure of the refinement relation is maintained, so if

`rewrite` rules can be disabled.

More will be written about this as we develop the techniques.