intro ⟨u,v, h1, h2, h3⟩
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (∃ u v, u ∈ L ∧ v ∈ epsilon ∧ w = u * v) → L w
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ L
h2 : v ∈ epsilon
h3 : w = u * v
⊢ L w