simp [Language.epsilon, Membership.mem] at h2
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
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ L
h2 : v = ε
h3 : w = u * v
⊢ L w