The Java null literal, as an ACL2 string.
Definition: *null-literal*
(defconst *null-literal* "null")
Theorem: ascii-listp-of-null-literal
(defthm ascii-listp-of-null-literal (ascii-listp (string=>unicode *null-literal*)))
