anchor.diff:    (define generate-hyp-hint-lst ((hyp-lst hint-pair-listp)
                                    (fn-lst func-alistp) (fn-lvls sym-nat-alistp))
       :returns (hyp-hint-lst hint-pair-listp)
  +    :enabled t
       (b* (((if (endp hyp-lst)) nil)
            ((cons (hint-pair hyp) rest) hyp-lst)
            (G-prim (car (expand (make-ex-args :term-lst (list hyp.thm)
  
positive.code:              (implies (and (pseudo-termp z) (consp z) (not (equal (car z) 'quote)))
                        (pseudo-term-listp (cdr z)))))
  
      (defthm cdar-of-ex-args->term-lst-is-pseudo-term-list
        (implies (and (ex-args-p expand-args)
                      (consp (ex-args->term-lst expand-args))
                      (consp (car (ex-args->term-lst expand-args)))
  
negative.code:     (defthm non-neg-of-cdr-of-hons-get-of-ex-args->fn-lvls-of-ex-args-p
        (implies (and (ex-args-p x) (hons-assoc-equal foo (ex-args->fn-lvls x)))
                 (<= 0 (cdr (hons-assoc-equal foo (ex-args->fn-lvls x)))))
        :hints(("Goal" :use ((:instance natp-of-cdr-of-hons-get-of-ex-args->fn-lvls-of-ex-args-p (x x))))))
      )
  
    (encapsulate
      ()
      (set-well-founded-relation l<)
  
      ;; Q FOR YAN:
      ;; 1. merge expand-args->fn-lst and expand-args->fn-lvls
      ;; 2. change update-fn-lvls function so that old items are not deleted and update the measure function
      ;; 3. clean the code in a more structured way - treat lambdas in another function
      ;; 4. clean up the above encapsulated theorems, maybe in another file
      (define expand ((expand-args ex-args-p))
        :returns (expanded-terms pseudo-term-listp
                                 :hints (("Goal" :in-theory (enable ex-args->term-lst))))
        :measure (expand-measure expand-args)
        :verify-guards nil
        :hints
        (("Goal"
          :use ((:instance sum-lvls-decrease-after-update
                           (fn (car (car (ex-args->term-lst expand-args))))
                           (fn-lvls (ex-args->fn-lvls expand-args))))))
        (b* ((expand-args (mbe :logic (ex-args-fix expand-args) :exec expand-args))
             ;; This binds expand-args to a, so that we can call a.term-lst ...
             ((ex-args a) expand-args)
             ((unless (consp a.term-lst)) nil)
             ((cons term rest) a.term-lst)
             ;; If first term is a symbolp, return the symbol
             ;; then recurse on the rest of the list
             ((if (symbolp term))
              (cons term (expand (change-ex-args a :term-lst rest))))
             ((if (equal (car term) 'quote))
              (cons term (expand (change-ex-args a :term-lst rest))))
             ;; The first term is now a function call:
             ;; Cons the function call and function actuals out of term
             ((cons fn-call fn-actuals) term)
  
             ;; If fn-call is a pseudo-lambdap
             ((if (pseudo-lambdap fn-call))
              (cons
               (b* ((lambda-formals (lambda-formals fn-call))
                    (lambda-body (car (expand (change-ex-args a :term-lst (list (lambda-body fn-call))))))
                    (lambda-actuals (expand (change-ex-args a :term-lst fn-actuals)))
                    ((unless (mbt (equal (len lambda-formals) (len lambda-actuals)))) nil))
                 `((lambda ,lambda-formals ,lambda-body) ,@lambda-actuals))
               (expand (change-ex-args a :term-lst rest))))
  
             ;; If fn-call is neither a lambda expression nor a function call
             ((unless (mbt (symbolp fn-call))) a.term-lst)
             ;; Try finding function call from fn-lst
             (fn (hons-get fn-call a.fn-lst))
             ;; If fn-call doesn't exist in fn-lst, it can be a basic function,
  