apply Set.eq_of_subset_of_subset
α : Type
L : Language α
⊢ kleene_closure α L = ⋃ n, exp L n
case a
α : Type
L : Language α
⊢ kleene_closure α L ⊆ ⋃ n, exp L n

case a
α : Type
L : Language α
⊢ ⋃ n, exp L n ⊆ kleene_closure α L