apply Exists.elim a1
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ s ∈ kleene_closure α L
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ ∀ (a : ℕ), s ∈ exp L a → s ∈ kleene_closure α L