case _ a2_left a2_right =>
  apply Exists.elim a2_right
  intro ys a3
  clear a2_right
  cases a3
  case _ a3_left a3_right =>
    simp only [← a3_right]
    apply kleene_closure.succ L
    apply ih xs a2_left
    exact a3_left
α : 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
no goals