anchor.diff:          :elt-type smtlink-option-name
           :true-listp t))
   
  -    (encapsulate ()
  -      (local (in-theory (enable smtlink-option-name-lst-fix)))
  -      (deffixtype smtlink-option-name-lst
  -        :pred  smtlink-option-name-lst-p
  -        :fix   smtlink-option-name-lst-fix
  -        :equiv smtlink-option-name-lst-equiv
  -        :define t
  -        :forward t
  -        :topic smtlink-option-name-lst-p))) ;; temporarily stop here
  -
       (defthm smtlink-option-name-fix-preserves-member
           (implies (member x used :test 'equal)
                    (member (smtlink-option-name-fix x)
  
positive.code:         :define t
          :forward t
          :topic smtlink-hint-syntax-p))
  ;;    )
  
    ;; -------------------------------------------------------------------------
  
  
negative.code:       :short "Fixing function for smtlink-hint-syntax."
        :returns (fixed-smtlink-hint-syntax smtlink-hint-syntax-p)
        (mbe :logic (if (smtlink-hint-syntax-p term) term nil)
             :exec term)
        ///
        (more-returns
         (fixed-smtlink-hint-syntax
          (implies (smtlink-hint-syntax-p term)
                   (equal fixed-smtlink-hint-syntax term))
          :hints(("Goal" :expand (smtlink-hint-syntax-p term)))
          :name
          smtlink-hint-syntax-fix-when-smtlink-hint-syntax-p)))
  
      (encapsulate ()
        (local (defthm lemma1
                 (implies (and (smtlink-hint-syntax-p term) term)
                          (and (mv-nth 0 (smtlink-option-syntax-p
                                          (list (car term) (cadr term)) nil))
                               (consp (cdr term))
                               (smtlink-hint-syntax-p (cddr term))
                               (true-listp term)))
                 :hints(("Goal"
                         :expand((smtlink-hint-syntax-p term)
                                 (smtlink-hint-syntax-p-helper term nil)
                                 (smtlink-hint-syntax-p (cddr term)))))))
  
        (local (defthmd lemma2
                 (implies (and (mv-nth 0 (smtlink-option-syntax-p term nil)) term)
                          (and (member-equal (car term) *smtlink-option-names*)
                               (or (and (equal (cdr (assoc-equal (car term) *smtlink-options*)) 'function-lst-syntax-p)
                                        (function-lst-syntax-p (cadr term)))
                                   (and (equal (cdr (assoc-equal (car term) *smtlink-options*)) 'hypothesis-lst-syntax-p)
                                        (hypothesis-lst-syntax-p (cadr term)))
                                   (and (equal (cdr (assoc-equal (car term) *smtlink-options*)) 'hints-syntax-p)
                                        (hints-syntax-p (cadr term)))
                                   (and (equal (cdr (assoc-equal (car term) *smtlink-options*)) 'booleanp)
                                        (booleanp (cadr term)))
                                   (and (equal (cdr (assoc-equal (car term) *smtlink-options*)) 'stringp)
                                        (stringp (cadr term)))
                                   (and (equal (cdr (assoc-equal (car term) *smtlink-options*)) 'smt-solver-params-p)
                                        (smt-solver-params-p (cadr term)))
                                   (and (equal (cdr (assoc-equal (car term) *smtlink-options*)) 'smt-solver-cnf-p)
                                        (smt-solver-cnf-p (cadr term))))))
                 :hints(("Goal" :expand((smtlink-option-syntax-p term nil)
                                        (:free (option-type) (eval-smtlink-option-type
                                                              option-type (cadr term)))
                                        (smtlink-option-name-p (car term)))))))
  
        (defthm everything-about-smtlink-syntax-p
          (implies (and (smtlink-hint-syntax-p term) term)
                   (let* ((opt (car term)) (val (cadr term)) (rest (cddr term))
                          (option-type (cdr (assoc-equal opt *smtlink-options*))))
                     (and (true-listp term)
                          (consp (cdr term))
                          (equal (smtlink-hint-syntax-fix term) term)
                          (smtlink-hint-syntax-p rest)
                          (member-equal opt *smtlink-option-names*)
                          (member-equal option-type *smtlink-option-types*)
                          (implies (equal option-type 'function-lst-syntax-p)
                                   (function-lst-syntax-p val))
                          (implies (equal option-type 'hypothesis-lst-syntax-p)
                                   (hypothesis-lst-syntax-p val))
                          (implies (equal option-type 'hints-syntax-p)
                                   (hints-syntax-p val))
                          (implies (equal option-type 'booleanp)
                                   (booleanp val))
                          (implies (equal option-type 'stringp)
                                   (stringp val))
                          (implies (equal option-type 'smt-solver-params-p)
                                   (smt-solver-params-p val))
                          (implies (equal option-type 'smt-solver-cnf-p)
                                   (smt-solver-cnf-p val)))))
          :hints(("Goal" :use((:instance lemma2 (term (list (car term) (cadr term))))))))
        )
  
      (encapsulate ()
        (local (in-theory (enable smtlink-hint-syntax-fix)))
  