clear a1
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
xs : List (List α)
a2 : (∀ r ∈ xs, r ∈ RegExp.languageOf α R) ∧ xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
case h.mp
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2 : (∀ r ∈ xs, r ∈ RegExp.languageOf α R) ∧ xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs