case _ a2_left a2_right =>
  simp only [← a2_right]
  cases xs
  case nil =>
    left
    simp
  case cons hd tl =>
    right
    simp at a2_left
    cases a2_left
    case _ a2_left_left a2_left_right =>
      apply Exists.intro hd
      tauto
α : 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
no goals