anchor.diff:    :hints (("Goal"
              :in-theory (e/d (function-option-lst-syntax-fix
                               function-option-lst-syntax-p
  -                            function-option-lst-syntax-p-helper
  -                            hypothesis-lst-syntax-p) (natp))
  -           :use ((:instance function-option-lst-syntax-p-of-option)
  -                 (:instance function-option-lst-syntax-p-constraint (any nil)))
  +                            function-option-syntax-p
  +                            hypothesis-lst-syntax-p)
  +                           (function-option-lst-syntax-p-helper--head
  +                            natp))
  +           :expand ((function-option-syntax-p (list (car fun-opt-lst) (cadr
  +                                                                       fun-opt-lst)) nil))
              )))
   
     (define make-merge-function ((func function-syntax-p) (smt-func func-p))
  
positive.code:     (mbe :logic (if (function-option-name-p option-name) option-name ':formals)
           :exec option-name))
  
  (encapsulate ()
    (local (in-theory (enable function-option-name-fix)))
    (deffixtype function-option-name
      :pred  function-option-name-p
      :fix   function-option-name-fix
      :equiv function-option-name-equiv
      :define t
      :forward t
      :topic function-option-name-p)
  
  (deflist function-option-name-lst
    :elt-type function-option-name
    :true-listp t))
  
    ;; (define function-option-name-lst-p ((option-lst t))
    ;;   :returns (syntax-good? booleanp)
    ;;   :short "Recoginizer for option-lst."
    ;;   (b* (((if (atom option-lst)) (equal option-lst nil))
    ;;        ((cons first rest) option-lst))
    ;;     (and (function-option-name-p first)
    ;;          (function-option-name-lst-p rest))))
  
    ;; (define function-option-name-lst-fix ((option-lst function-option-name-lst-p))
    ;;   :returns (fixed-option-lst function-option-name-lst-p
    ;;                              :hints (("Goal" :in-theory (enable function-option-name-lst-p))))
    ;;   :short "Fixing function for option-name-lst."
    ;;   :verify-guards nil
    ;;   (mbe :logic (if (atom option-lst)
    ;;                   nil
    ;;                 (cons (function-option-name-fix (car option-lst))
    ;;                       (function-option-name-lst-fix (cdr option-lst))))
    ;;        :exec option-lst))
    ;; (verify-guards function-option-name-lst-fix
    ;;   :hints (("Goal" :in-theory (enable function-option-name-fix
    ;;                                      function-option-name-lst-fix
    ;;                                      function-option-name-p function-option-name-lst-p))))
  
    ;; The conditions in eval-type should go along with *function-options*
    (define eval-function-option-type ((option-type function-option-type-p) (term t))
      :returns (type-correct? booleanp)
      :short "Evaluating types for function option body."
      (b* ((option-type (function-option-type-fix option-type)))
        (case option-type
          (argument-lst-syntax-p (argument-lst-syntax-p term))
          (natp (natp term))
          (hypothesis-syntax-p (hypothesis-syntax-p term))
          (t (hypothesis-lst-syntax-p term)))))
  
    (define function-option-syntax-p ((term t) (used function-option-name-lst-p))
      :returns (mv (syntax-good? booleanp)
                   (used? function-option-name-lst-p
                          :hints (("Goal" :in-theory (enable function-option-name-lst-p function-option-name-p)))))
      :short "Recoginizer for function-option-syntax."
      :verify-guards nil
      (b* ((used (function-option-name-lst-fix used))
           ((if (equal term nil)) (mv t used))
           ((unless (and (true-listp term) (car term) (not (cddr term)))) (mv nil used))
           ((cons option body-lst) term)
           ((unless (function-option-name-p option)) (mv nil used))
           (option-type (cdr (assoc-equal option *function-options*))))
        (mv (and (not (member-equal option used))
                 (eval-function-option-type option-type (car body-lst)))
            (cons option used))))
    (verify-guards function-option-syntax-p
      :guard-debug t
      :hints (("Goal" :in-theory (enable function-option-syntax-p function-option-name-p
                                         eval-function-option-type function-option-name-lst-p))))
  
    ;; (define exist-odd-lst ((key symbolp) (lst t))
    ;;   :returns (exist? booleanp)
    ;;   :short "Test if key exist in lst on the odd positions (with position staring
    ;; from 1)"
    ;;   :measure (len lst)
    ;;   :hints (("Goal" :in-theory (enable true-list-fix)))
    ;;   :verify-guards nil
    ;;   (b* ((key (symbol-fix key))
    ;;        ((if (equal lst nil)) nil)
    ;;        ((unless (and (true-listp lst) (>= (len lst) 2))) nil)
    ;;        ((list* first & rest) lst)
    ;;        ((if (equal first key)) t))
    ;;     (exist-odd-lst key rest)))
    ;; (verify-guards exist-odd-lst
    ;;   :hints (("Goal" :in-theory (enable true-list-fix))))
  
  (define function-option-lst-syntax-p-helper ((term t) (used function-option-name-lst-p))
      :returns (syntax-good? booleanp)
      :short "Helper for function-option-lst-syntax-p."
      (b* (((if (atom term)) (equal term nil))
           ((unless (and (true-listp term) (>= (len term) 2))) nil)
           ((list* first second rest) term)
           (- (cw "first: ~q0" first))
           (- (cw "second: ~q0" second))
           ((mv res new-used) (function-option-syntax-p (list first second)
                                                        used))
           (- (cw "res: ~q0" res))
           (- (cw "booleanp? ~q0" (booleanp second))))
        (and res (function-option-lst-syntax-p-helper rest new-used)))
      ///
      (defthm function-option-lst-syntax-p-constraint
        (implies (and (function-option-lst-syntax-p-helper fun-opt-lst any)
                      (consp fun-opt-lst))
                 (or (equal (car fun-opt-lst) ':formals)
                     (equal (car fun-opt-lst) ':returns)
                     (equal (car fun-opt-lst) ':level)
                     (equal (car fun-opt-lst) ':guard)
                     (equal (car fun-opt-lst) ':more-returns)))
        :hints (("Goal"
                 :in-theory (enable eval-function-option-type
                                    function-option-syntax-p
                                    function-option-name-p))))
  
      (defthm function-option-lst-syntax-p-of-option
        (implies
         (and (consp (cdr fun-opt-lst))
              (function-option-lst-syntax-p-helper fun-opt-lst nil)
              (consp fun-opt-lst))
         (and (implies (equal (car fun-opt-lst) ':formals)
                       (argument-lst-syntax-p (cadr fun-opt-lst)))
              (implies (equal (car fun-opt-lst) ':returns)
                       (argument-lst-syntax-p (cadr fun-opt-lst)))
              (implies (equal (car fun-opt-lst) ':level)
                       (natp (cadr fun-opt-lst)))
              (implies (equal (car fun-opt-lst) ':guard)
                       (hypothesis-syntax-p (cadr fun-opt-lst)))
              (implies (equal (car fun-opt-lst) ':more-returns)
                       (hypothesis-lst-syntax-p (cadr fun-opt-lst)))))
        :hints (("Goal"
                 :in-theory (enable function-option-syntax-p
                                    eval-function-option-type))))
  
      (defthm car-term-function-option-syntax-p
        (implies (and (consp term)
                      (function-option-lst-syntax-p-helper term used))
                 (function-option-name-p (car term)))
        :hints (("Goal" :in-theory (enable function-option-syntax-p))))
  
      (defthm caddr-term-function-option-syntax-p
        (implies (and (consp (cddr term))
                      (not (function-option-name-p (caddr term)))
                      (function-option-lst-syntax-p-helper (cddr term) used))
                 (not (caddr term)))
        :hints (("Goal" :in-theory (enable function-option-syntax-p))))
      )
  
  (define true-set-equiv ((list1 true-listp) (list2 true-listp))
    :returns (p booleanp)
    (if (equal (true-listp list1) (true-listp list2))
  
negative.code:                                        hypothesis-lst-syntax-fix
                                         hypothesis-syntax-p
                                         hypothesis-syntax-fix))))
    )
  
  
  (working-here)
  (defthm function-option-lst-syntax-p-implies-everything-you-want
    (implies (and (function-option-lst-syntax-p term) term)
             (and (function-option-syntax-p (list (car term) (cadr term)) nil)))
    :hints(("Goal"
            :expand((function-option-lst-syntax-p term)
                    (function-option-lst-syntax-p-helper term nil))
            :use ((:instance function-option-lst-syntax-p-helper--monotonicity
                             (term (cddr term)))))))
  
    ;; Bozo:
    ;; This implementation is potentially slow because of the threading of smt-func
    ;; all the way while at the same time updating it.
    (define make-merge-function-option-lst ((fun-opt-lst function-option-lst-syntax-p)
  