anchor.diff:      :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)
  -                                            :fn-lst fn-lst
  -                                            :fn-lvls fn-lvls
  -                                            :wrld-fn-len wrld-fn-len) state))))
  +         (expand-result
  +          (expand (make-ex-args :term-lst (list hyp.thm)
  +                                :fn-lst fn-lst
  +                                :fn-lvls fn-lvls
  +                                :wrld-fn-len wrld-fn-len) state))
  +         ((ex-outs e) expand-result)
  +         (G-prim (car e.expanded-term-lst)))
         (cons (make-hint-pair :thm G-prim
                               :hints hyp.hints)
               (generate-hyp-hint-lst rest fn-lst fn-lvls wrld-fn-len state))))
  
positive.code: 
             ;; Expand main clause using fn-lst
             ;; Generate function hypotheses and their hints from fn-lst
             (G-prim
              (with-fast-alist fn-lst
                (car (expand (make-ex-args
                              :term-lst (list (disjoin cl))
                              :fn-lst fn-lst
                              :fn-lvls fn-lvls
                              :wrld-fn-len wrld-fn-len)
                             state))))
  
             ;; Generate auxiliary hypotheses from function expansion
             (fn-hint-lst (with-fast-alist fn-lst (generate-fn-hint-lst (make-fhg-args
  
negative.code:       (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))
              (make-ex-outs :expanded-term-lst nil :expanded-fn-lst a.expand-lst))
             ((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))
              (b* ((rest-res (expand (change-ex-args a :term-lst rest) state))
                   ((ex-outs o) rest-res))
                (make-ex-outs :expanded-term-lst (cons term o.expanded-term-lst)
                              :expanded-fn-lst o.expanded-fn-lst)))
             ((if (equal (car term) 'quote))
              (b* ((rest-res (expand (change-ex-args a :term-lst rest) state))
                   ((ex-outs o) rest-res))
                (make-ex-outs :expanded-term-lst (cons term o.expanded-term-lst)
                              :expanded-fn-lst o.expanded-fn-lst)))
             ;; 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))
              (b* ((lambda-formals (lambda-formals fn-call))
                   (body-res
                    (expand (change-ex-args a :term-lst (list (lambda-body fn-call))) state))
                   ((ex-outs b) body-res)
                   (lambda-body (car b.expanded-term-lst))
                   (actuals-res
                    (expand (change-ex-args a :term-lst fn-actuals :expand-lst b.expanded-fn-lst) state))
                   ((ex-outs ac) actuals-res)
                   (lambda-actuals ac.expanded-term-lst)
                   ((unless (mbt (equal (len lambda-formals) (len lambda-actuals))))
                    (make-ex-outs :expanded-term-lst a.term-lst :expanded-fn-lst a.expand-lst))
                   (lambda-fn `((lambda ,lambda-formals ,lambda-body) ,@lambda-actuals))
                   (rest-res
                    (expand (change-ex-args a :term-lst rest :expand-lst ac.expanded-fn-lst) state))
                   ((ex-outs r) rest-res))
                (make-ex-outs :expanded-term-lst (cons lambda-fn r.expanded-term-lst)
                              :expanded-fn-lst r.expanded-fn-lst)))
  
             ;; If fn-call is neither a lambda expression nor a function call
             ((unless (mbt (symbolp fn-call)))
              (make-ex-outs :expanded-term-lst a.term-lst :expanded-fn-lst a.expand-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,
  