Recognize true lists of well-formed event forms.
Function:
(defun pseudo-event-form-listp (x) (declare (xargs :guard t)) (if (atom x) (equal x nil) (and (pseudo-event-formp (car x)) (pseudo-event-form-listp (cdr x)))))
Theorem:
(defthm true-listp-when-pseudo-event-form-listp-rewrite (implies (pseudo-event-form-listp x) (true-listp x)))