cons-listp

(in-package "ACL2")

(deflist cons-listp
  (x)
  (consp x)
  :elementp-of-nil nil
  :cheap t
  :parents (std/typed-lists alistp)
  :short "Like @(see alistp) but doesn't require that the final cdr is @('nil').")

(deflist cons-list-listp
  (x)
  (cons-listp x)
  :parents (std/typed-lists)
  :elementp-of-nil t)