simp only [thm_5 L] at a1_right
α : Type
L : Language α
x : Str α
a1_right : x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
α : Type
L : Language α
x : Str α
a1_right : x ∈ concat L (⋃ n, exp L n)
⊢ x ∈ kleene_closure α L