cases a1
case a
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
case a.intro
α : Type
L : Language α
s : Str α
w✝ : ℕ
h✝ : s ∈ exp L w✝
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)