case succ k ih =>
  simp only [exp]
  conv => left; simp only [ih]
  simp only [thm_3_c]
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (exp L (k + 1)) L = concat L (exp L (k + 1))
no goals