theorem EDT0LGrammar.terminal_word_count {T : Type u_1} {N : Type u_2} (w : List T) : List.countP SymbolIsNonterminal (List.map Symbol.terminal w) = 0

theorem EDT0LGrammar.regular_languages_are_fi_edt0l {T : Type u_1} [Fintype T] (L : Language T) : L.IsRegular → L.IsEDT0LOfIndex 1