simp only [← a2_right]
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ xs.join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = xs.join