. intros; exact Sigma.kleene_contains_all w
case h.mp
α : Type u_1
w : Word α
⊢ w ∈ univ → w ∈ (Σ)∗

case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ
case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ