apply Exists.intro ys
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ t ∈ L, xs ++ t = xs ++ ys
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ys ∈ L ∧ xs ++ ys = xs ++ ys