anchor.diff:                 (:instance booleanp-of-function-option-syntax-p.syntax-good?
                             (used used-2) (term (list opt val)))))))
   
  -  (Defthm lemma-2
  +  (defthm lemma-2
       (implies (and (function-option-name-lst-p used)
                     (function-option-name-p new-opt)
                     (mv-nth 0 (function-option-syntax-p (list opt val)
  
positive.code:                          (function-option-name-lst-p used-2))))
    :rule-classes(:congruence))
  
  (failed-here)
  (defthm lemma-1
    (implies (member x used :test 'equal)
             (member (function-option-name-fix x)
                     (function-option-name-lst-fix used) :test 'equal)))
  (defthm lemma-2
    (implies (and (subsetp used-1 used-2 :test 'equal)
                  (consp used-1))
             (member (function-option-name-fix (car used-1))
                     (function-option-name-lst-fix used-2)))
    :hints(("Goal" :in-theory (enable function-option-name-lst-fix))))
  
  (defthm lemma-3
    (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 (function-option-name-lst-fix
                                    function-option-name-fix) ))))
  
  (defthm function-option-syntax-p--monotonicity
    (implies (and (equal (true-listp used-1) (true-listp used-2))
  
negative.code: (defthm function-option-syntax-p--congruence
    (implies (and (function-option-name-lst-p used-1)
                  (function-option-name-lst-p used-2)
                  (acl2::set-equiv used-1 used-2))
             (equal (mv-nth 0 (function-option-syntax-p (list opt val)
                                                        used-1))
                    (mv-nth 0 (function-option-syntax-p (list opt val)
                                                        used-2))))
    :hints(("Goal" :in-theory (disable function-option-syntax-p--monotonicity
                                       booleanp-of-function-option-syntax-p.syntax-good?)
            :use((:instance function-option-syntax-p--monotonicity
  