case _ a2_left_left a2_left_right =>
  apply Exists.intro hd
  tauto
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left_left : hd ∈ RegExp.languageOf α R
a2_left_right : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
no goals