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 hd : List α
tl : List (List α)
a2_left : ∀ r ∈ hd :: tl, r ∈ RegExp.languageOf α R
a2_right : (hd :: tl).join = cs
⊢ (hd :: tl).join = [] ∨
    ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
no goals