apply ih xs a2_left
case a
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ xs ∈ kleene_closure α L

case a
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ ys ∈ L
case a
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
ys : Str α
a3_left : ys ∈ L
a3_right : xs ++ ys = s
⊢ ys ∈ L