constructor
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} ↔ w ∈ L∗
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} → w ∈ L∗

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}