induction n generalizing s
α : Type
L : Language α
n : ℕ
s : Str α
a1 : s ∈ exp L n
⊢ s ∈ kleene_closure α L
case zero
α : Type
L : Language α
s : Str α
a1 : s ∈ exp L 0
⊢ s ∈ kleene_closure α L

case succ
α : Type
L : Language α
n✝ : ℕ
a✝ : ∀ s ∈ exp L n✝, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ exp L (n✝ + 1)
⊢ s ∈ kleene_closure α L