intro s a1
case a
α : Type
L : Language α
⊢ ∀ x ∈ kleene_closure α L, x ∈ {[]} ∪ concat L (kleene_closure α L)
case a
α : Type
L : Language α
s : Str α
a1 : s ∈ kleene_closure α L
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)