anchor.diff:  (defthm alistp-make-alist
     (alistp (make-alist a b)))
   
  -(defun sub-type-case-1 (rst-type-case var-alist)
  -  (declare (xargs :mode :program))
  -  (cond ((atom rst-type-case) nil)
  -        ((consp (car rst-type-case))
  -         (cons (appsyms (append
  -                         (cons (caar rst-type-case)
  -                               (sub-type-case-1 (cdar rst-type-case)
  -                                                var-alist))
  -                         '(p)))
  -               (sub-type-case-1 (cdr rst-type-case) var-alist)))
  -        (t (let ((var-sub (assoc-equal (car rst-type-case) var-alist)))
  -             (if var-sub
  -                 (cons (cdr var-sub) (sub-type-case-1 (cdr rst-type-case) var-alist))
  -                 (cons (car rst-type-case)
  -                       (sub-type-case-1 (cdr rst-type-case) var-alist)))))))
  -  
  +(mutual-recursion
  +
  + (defun subst-type-name (type var-alist)
  +   (declare (xargs :mode :program))
  +   (cond ((atom type)
  +          (let ((var-sub (assoc-equal type var-alist)))
  +            (if var-sub
  +                (cdr var-sub)
  +              type)))
  +         (t (appsyms (cons (car type)
  +                           (map-subst-type-name (cdr type) var-alist))))))
  +
  + (defun map-subst-type-name (types var-alist)
  +   (declare (xargs :mode :program))
  +   (cond ((atom types) nil)
  +         (t (cons (subst-type-name (car types) var-alist)
  +                  (map-subst-type-name (cdr types) var-alist))))))
  +
  +;; (defun sub-type-case-1 (rst-type-case var-alist)
  +;;   (declare (xargs :mode :program))
  +;;   (cond ((atom rst-type-case) nil)
  +;;         ((consp (car rst-type-case))
  +;;          (cons (appsyms (append
  +;;                          (cons (caar rst-type-case)
  +;;                                (sub-type-case-1 (cdar rst-type-case)
  +;;                                                 var-alist))))
  +;;                (sub-type-case-1 (cdr rst-type-case) var-alist)))
  +;;         (t (let ((var-sub (assoc-equal (car rst-type-case) var-alist)))
  +;;              (if var-sub
  +;;                  (cons (cdr var-sub) (sub-type-case-1 (cdr rst-type-case) var-alist))
  +;;                  (cons (car rst-type-case)
  +;;                        (sub-type-case-1 (cdr rst-type-case) var-alist)))))))
  +
  +(defun add-p-to-list (symlist)
  +  (declare (xargs :mode :program
  +                  :guard (symbol-listp symlist)))
  +  (cond ((atom symlist) nil)
  +        (t (cons (appsyms (list (car symlist) 'p))
  +                 (add-p-to-list (cdr symlist))))))
  +
   (defun sub-type-case (type-case var-alist)
     (declare (xargs :mode :program))
     (cons (appsyms (cons (car type-case) (strip-cdrs var-alist)))
  -        (sub-type-case-1 (cdr type-case) var-alist)))
  +        (add-p-to-list (map-subst-type-name (cdr type-case) var-alist))))
   
   (defun sub-type-cases (type-cases var-alist)
     (declare (xargs :mode :program))
  
positive.code:         (t (get-body-declare (cddr rst)))))
  
  (defmacro defthm-typed (name typed-vars term &rest rst)
    (list 'progn
          (append (list 'defund-typed
                        (hyphenate-symbols (list name 'body))
  
negative.code: ;;        (restriction x)))
  
  (defmacro defsubtype (subtype-p parenttype-p restriction)
    (declare (xargs :guard (and (symbolp subtype-p)
                                (symbolp parenttype-p))))
    `(progn
       (defpredicate ,subtype-p (x)
         (and (,parenttype-p x)
  