Lemmas about true-listp available in the std/lists library.
Note: the list of lemmas below is quite incomplete. For instance, the true-listp rule about append will be found in the documentation for std/lists/append, instead of here.
(defthm true-listp-when-atom (implies (atom x) (equal (true-listp x) (not x))))
(defthm true-listp-of-cons (equal (true-listp (cons a x)) (true-listp x)))
(defthm consp-under-iff-when-true-listp (implies (true-listp x) (iff (consp x) x)) :rule-classes ((:rewrite :backchain-limit-lst 0)))