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