simp only [exp]
α : 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))
α : Type
L : Language α
k : ℕ
ih : concat (exp L k) L = concat L (exp L k)
⊢ concat (concat (exp L k) L) L = concat L (concat (exp L k) L)