intro
| Exists.intro nn r =>
  cases nn with
  | succ m =>
    apply Or.inl
    unfold Language.plus
    exists (Nat.succ m)
    exact ⟨Nat.succ_ne_zero m, r⟩
  | zero =>
    apply Or.inr
    exact r
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ kstar L → w ∈ L⁺ ∪ {ε}
no goals