avoiding :use hints for enabled :rewrite rules

Consider the following (admittedly silly) example.

(thm (equal (append (append x y) z) (append x y z))
     :hints (("Subgoal *1/1" :use cdr-cons)))
ACL2's output includes the following warning.
ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE an enabled
:REWRITE or :DEFINITION rule, so you may want to consider disabling
(:REWRITE CDR-CONS) in the hint provided for Subgoal *1/1.
The warning is saying that if you leave the rewrite rule enabled, ACL2 may simplify away the hypothesis added by the :use hint. We now explain this danger in more detail and show how disabling the rule can solve this problem.

Recall (see hints) how :use hints work. Such a hint specifies a formula, F, which is based on an existing lemma. Then the indicated goal, G, is replaced by the implication (implies F G). The intention is that the truth of F will help in the simplification of G to T (true). The ``[Use]'' warning shown above is telling us of the danger that F may be rewritten to T, reducing the implication above to (implies T G) -- thus, sadly, F has disappeared and is not available to help with the simplification of G.

Consider the following tiny example.

  (defun p (x) (cons x x))
  (defthm car-p
     (equal (car (p x)) x))
  (in-theory (disable p (:type-prescription p)))
  (thm (implies (equal (p x1) (p x2))
                (equal x1 x2))
       :hints (("Goal"
                :use ((:instance car-p (x x1))
                      (:instance car-p (x x2))))))
The proof of the final thm form fails, because the new hypotheses are rewritten to t using the :rewrite rule CAR-P, in the manner described above. The following proof log shows the new hypotheses and their disappearance via rewriting.
  We augment the goal with the hypotheses provided by the :USE hint.
  These hypotheses can be derived from CAR-P via instantiation.  We are
  left with the following subgoal.

                (EQUAL (CAR (P X2)) X2))
           (IMPLIES (EQUAL (P X1) (P X2))
                    (EQUAL X1 X2))).

  By the simple :rewrite rule CAR-P we reduce the conjecture to

  (IMPLIES (EQUAL (P X1) (P X2))
           (EQUAL X1 X2)).
When we disable the rule CAR-P as follows, the proof succeeds.
  (thm (implies (equal (p x1) (p x2))
                (equal x1 x2))
       :hints (("Goal"
                :use ((:instance car-p (x x1))
                      (:instance car-p (x x2)))
                :in-theory (disable car-p))))
In general, then, a solution is to disable the rewrite rule that you are supplying in a :use hint.