. simp [KStar.kstar]
  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 ∈ L∗ → w ∈ L⁺ ∪ {ε}
no goals