cases a2
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2 : xs ∈ exp L n ∧ ∃ t ∈ L, xs ++ t = s
⊢ s ∈ kleene_closure α L
case intro
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
left✝ : xs ∈ exp L n
right✝ : ∃ t ∈ L, xs ++ t = s
⊢ s ∈ kleene_closure α L