arglistp

(in-package "ACL2")

(defsection std/system/arglistp
  :parents (std/system)
  :short "Theorems about @(tsee arglistp)."
  (defthm true-listp-when-arglistp
    (implies (arglistp x) (true-listp x))
    :rule-classes :compound-recognizer))