ext cs
α : Type
R : RegExp α
⊢ RegExp.languageOf α R.closure = RegExp.languageOf α (RegExp.epsilon.union (R.concat R.closure))
case h
α : Type
R : RegExp α
cs : List α
⊢ cs ∈ RegExp.languageOf α R.closure ↔ cs ∈ RegExp.languageOf α (RegExp.epsilon.union (R.concat R.closure))