simp only [Set.subset_def]
case a
α : Type
L : Language α
⊢ {[]} ∪ concat L (kleene_closure α L) ⊆ kleene_closure α L
case a
α : Type
L : Language α
⊢ ∀ x ∈ {[]} ∪ concat L (kleene_closure α L), x ∈ kleene_closure α L