(in-package "ACL2")
(local (include-book "kestrel/lists-light/nth" :dir :system))
(defthm characterp-of-char (equal (characterp (char s n)) (and (stringp s) (< (nfix n) (length s)))) :hints (("Goal" :cases ((characterp (nth n (coerce s 'list)))))))