case succ n ih =>
  simp only [exp] at a1
  simp only [concat] at a1
  simp at a1
  apply Exists.elim a1
  intro xs a2
  clear a1
  cases a2
  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 : Str α
a1 : s ∈ exp L (n + 1)
⊢ s ∈ kleene_closure α L
no goals