cases a2_left
case h
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left : hd ∈ RegExp.languageOf α R ∧ ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
case h.intro
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
left✝ : hd ∈ RegExp.languageOf α R
right✝ : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join