simp only [exp] at a1
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ exp L (n + 1)
⊢ s ∈ kleene_closure α L
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ concat (exp L n) L
⊢ s ∈ kleene_closure α L