apply Exists.intro []
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ (∀ r ∈ [], r ∈ RegExp.languageOf α R) ∧ [].join = cs