unfold Language.plus
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ L⁺
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ fun w => ∃ n, ¬n = 0 ∧ w ∈ L ^ n