theorem trivial_EDT0L_grammars {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] [IsEmpty H] (E : EDT0LGrammar T N H) : E.language = 0

theorem empty_language_is_EDT0L {α : Type u_1} : Language.IsEDT0L 0

theorem language_1_is_EDT0L {α : Type u_1} : Language.IsEDT0L 1