The singleton-word language is context-sensitive

theorem singletonWordLanguage_is_CS {T : Type} [Fintype T] (w : List T) : is_CS (singletonWordLanguage w)

The singleton-word language {w} is context-sensitive.