simp only [concat] at a1
α : 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
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s : Str α
a1 : s ∈ {x | ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = x}
⊢ s ∈ kleene_closure α L