Built-in axioms and theorems about values amenable to eql.
Theorem:
(defthm eqlablep-recog (equal (eqlablep x) (or (acl2-numberp x) (symbolp x) (characterp x))) :rule-classes :compound-recognizer)
Theorem:
(defthm eqlablep-nth (implies (eqlable-listp x) (eqlablep (nth n x))))