theorem EDT0LGrammar.UnionData.extend_alphabet₀_is_nonterminal {T : Type u_1} {N₀ : Type u_2} {N₁ : Type u_3} (s : Symbol T N₀) : SymbolIsNonterminal s = SymbolIsNonterminal (extend_alphabet₀ s)

theorem EDT0LGrammar.UnionData.extend_alphabet₁_is_nonterminal {T : Type u_1} {N₀ : Type u_2} {N₁ : Type u_3} (s : Symbol T N₁) : SymbolIsNonterminal s = SymbolIsNonterminal (extend_alphabet₁ s)

theorem EDT0LGrammar.UnionData.extend_alphabet₀_map_count {T : Type u_1} {N₀ : Type u_2} {N₁ : Type u_3} (w : List (Symbol T N₀)) : List.countP SymbolIsNonterminal w = List.countP SymbolIsNonterminal (List.map extend_alphabet₀ w)

theorem EDT0LGrammar.UnionData.extend_alphabet₁_map_count {T : Type u_1} {N₀ : Type u_2} {N₁ : Type u_3} (w : List (Symbol T N₁)) : List.countP SymbolIsNonterminal w = List.countP SymbolIsNonterminal (List.map extend_alphabet₁ w)

theorem EDT0LGrammar.UnionData.closed_under_union' {T : Type u_1} {N₀ : Type u_2} {H₀ : Type u_3} {N₁ : Type u_4} {H₁ : Type u_5} [Fintype N₀] [Fintype H₀] [Fintype N₁] [Fintype H₁] (𝓖 : UnionData) {k₁ k₂ : ℕ} (h₀ : 𝓖.E₀.IsIndex k₁) (h₁ : 𝓖.E₁.IsIndex k₂) : 𝓖.grammar.IsIndex (k₁.max k₂)

theorem EDT0LGrammar.finite_index_closed_under_union {T : Type u_1} {k₁ k₂ : ℕ} (L₁ L₂ : Language T) (h₁ : L₁.IsEDT0LOfIndex k₁) (h₂ : L₂.IsEDT0LOfIndex k₂) : (L₁ + L₂).IsEDT0LOfIndex (k₁.max k₂)