Some theorems about lists whose lengths are (i) equal, (ii) equal or above, or (iii) above constant values.
These theorems are disabled by default. They can be enabled to turn assertions about lengths and constants into assertions about consp and cdr: the expansion terminates because of the syntaxp restriction.
(defthm equal-len-const (implies (syntaxp (quotep c)) (equal (equal (len x) c) (if (natp c) (if (equal c 0) (not (consp x)) (and (consp x) (equal (len (cdr x)) (1- c)))) nil))))
(defthm gteq-len-const (implies (syntaxp (quotep c)) (equal (>= (len x) c) (or (<= (fix c) 0) (and (consp x) (>= (len (cdr x)) (1- c)))))))