Theorems about results of std/strings functions that return lists of binary digit characters.
Those std/strings are accompanied by theorems that they return bin-digit-char-list*p, but they in fact return true lists, so here we add theorems that they return bin-digit-char-listp.
Theorem:
(defthm bin-digit-char-listp-of-basic-nat-to-bin-chars (bin-digit-char-listp (basic-nat-to-bin-chars nat)))
Theorem:
(defthm bin-digit-char-listp-of-nat-to-bin-chars-aux (implies (bin-digit-char-listp acc) (bin-digit-char-listp (nat-to-bin-chars-aux nat acc))))
Theorem:
(defthm bin-digit-char-listp-of-nat-to-bin-chars (bin-digit-char-listp (nat-to-bin-chars nat)))