The singleton empty-word language is regular

emptyWordLanguage T = {[]} is regular (it is Language.isRegular_epsilon), and so is its complement.

theorem emptyWordLanguage_isRegular {T : Type} : (emptyWordLanguage T).IsRegular

The singleton empty-word language is regular.

theorem emptyWordLanguage_compl_isRegular {T : Type} : (emptyWordLanguage T)ᶜ.IsRegular

The complement of the singleton empty-word language is regular.