apply Exists.elim a2_right
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
a2_right : ∃ t ∈ L, xs ++ t = s
⊢ s ∈ kleene_closure α L
α : Type
L : Language α
n : ℕ
ih : ∀ s ∈ exp L n, s ∈ kleene_closure α L
s xs : Str α
a2_left : xs ∈ exp L n
a2_right : ∃ t ∈ L, xs ++ t = s
⊢ ∀ (a : Str α), a ∈ L ∧ xs ++ a = s → s ∈ kleene_closure α L