Inversion theorems for implode and explode.
Theorem: explode-of-implode
(defthm explode-of-implode (equal (explode (implode x)) (if (stringp x) nil (make-character-list x))))
Theorem: implode-of-explode
(defthm implode-of-explode (equal (implode (explode x)) (if (stringp x) x "")))
