apply-constraints

(encapsulate ((badge-userfn (fn) t))
  (local (defun badge-userfn (fn) (declare (ignore fn)) nil))
  (defthm badge-userfn-type
    (implies (badge-userfn fn)
      (apply$-badgep (badge-userfn fn)))
    :rule-classes ((:forward-chaining))))

(encapsulate ((apply$-userfn (fn args) t :guard (true-listp args)))
  (local (defun apply$-userfn
      (fn args)
      (declare (ignore fn args))
      nil))
  (defthm apply$-userfn-takes-arity-args
    (implies (badge-userfn fn)
      (equal (apply$-userfn fn args)
        (apply$-userfn fn
          (take (apply$-badge-arity (badge-userfn fn)) args))))
    :rule-classes nil))

(encapsulate (((untame-apply$ * *) =>
     *
     :formals (fn args)
     :guard (true-listp args)))
  (local (defun untame-apply$
      (fn args)
      (declare (ignore fn args))
      nil))
  (defthm untame-apply$-takes-arity-args
    (implies (badge-userfn fn)
      (equal (untame-apply$ fn args)
        (untame-apply$ fn
          (take (apply$-badge-arity (badge-userfn fn)) args))))
    :rule-classes ((:rewrite :corollary (implies (and (syntaxp (and (quotep fn) (symbolp args)))
           (badge-userfn fn))
         (equal (untame-apply$ fn args)
           (untame-apply$ fn
             (take (apply$-badge-arity (badge-userfn fn)) args))))))))