(vl-genblob-elementlist-count x) → count
Theorem:
(defthm vl-genblob-elementlist-count-greater-than-genblob-count (b* ((common-lisp::?count (vl-genblob-elementlist-count x))) (< (vl-genblob-count (vl-sort-genelements x)) count)) :rule-classes :linear)