anchor.diff:  
     (def-join-thms ev-process-hint)
   
  +(encapsulate ()
     (local (in-theory (enable process-hint)))
     (defthm correctness-of-process-hint
       (implies (and (pseudo-term-listp cl)
  
positive.code:                    (conjoin-clauses (process-hint cl hint))
                     b))
               (ev-process-hint (disjoin cl) b))
      :rule-classes :clause-processor)
  
    ;; Smtlink is a macro that generates a clause processor hint. This clause
    ;;   processor hint generates a clause, with which a new smt-hint is attached.
  
negative.code:                          (function-option-name-lst-p used-2))))
    :rule-classes(:congruence))
  
  (defthm function-option-name-fix-preserve-member
    (implies (member x used :test 'equal)
             (member (function-option-name-fix x)
                     (function-option-name-lst-fix used) :test 'equal)))
  
  (defthm function-option-name-lst-fix-preserve-subsetp
    (implies (subsetp used-1 used-2 :test 'equal)
             (subsetp (function-option-name-lst-fix used-1)
                      (function-option-name-lst-fix used-2)
                      :test 'equal))
    :hints(("Goal" :in-theory (e/d (subsetp-equal)))))
  
  (defthm function-option-syntax-p--monotonicity
    (implies (and (equal (true-listp used-1) (true-listp used-2))
  