nats=>chars and chars=>nats are mutual inverses.
Theorem:
(defthm chars=>nats-of-nats=>chars (implies (unsigned-byte-listp 8 (true-list-fix nats)) (equal (chars=>nats (nats=>chars nats)) (true-list-fix nats))) :rule-classes ((:rewrite :corollary (implies (unsigned-byte-listp 8 nats) (equal (chars=>nats (nats=>chars nats)) nats)))))
Theorem:
(defthm nats=>chars-of-chars=>nats (equal (nats=>chars (chars=>nats chars)) (make-character-list chars)))