A rule list is well-formed iff all its rules are well-formed, there are no duplicate rules, and incremental rules follow non-incremental rules.
The first condition is structural. The second condition is justifiable because duplicate rules are redundant. The third condition is reasonably implied by [RFC:3.3].
Non-emptiness is not required by the rule
(defun rulelist-wfp (rules) (declare (xargs :guard (rulelistp rules))) (and (rule-list-wfp rules) (no-duplicatesp-equal rules) (rulelist-incremental-ok-p rules)))
(defthm booleanp-of-rulelist-wfp (b* ((yes/no (rulelist-wfp rules))) (booleanp yes/no)) :rule-classes :rewrite)