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

A rewrite rule may fail to fire because its equivalence relation is not
known to be a refinement of any of those known to be permitted. See `geneqv` for a discussion of how ACL2 uses `congruence` rules to derive
the permitted equivalences and how those equivalences are represented. See
refinement-failure for advice on how to use break-rewrite to
determine that a rule failed the refinement check and for advice about how to
``fix'' such a problem.

`rewrite` rules can be disabled.

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