The singleton-word language is recursively enumerable

theorem singletonWordLanguage_is_RE {T : Type} [Fintype T] (w : List T) : is_RE (singletonWordLanguage w)

The singleton-word language {w} is recursively enumerable, via CF ⊆ RE.