induction n
α : Type
L : Language α
n : ℕ
⊢ concat (exp L n) L = concat L (exp L n)
case zero
α : Type
L : Language α
⊢ concat (exp L 0) L = concat L (exp L 0)

case succ
α : Type
L : Language α
n✝ : ℕ
a✝ : concat (exp L n✝) L = concat L (exp L n✝)
⊢ concat (exp L (n✝ + 1)) L = concat L (exp L (n✝ + 1))