simp at a1
case a
α : Type
L : Language α
x : Str α
a1 : x ∈ {[]} ∪ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
case a
α : Type
L : Language α
x : Str α
a1 : x = [] ∨ x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L