simp [Language.epsilon, Membership.mem] at h1
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u ∈ epsilon
h2 : v ∈ L
h3 : w = u * v
⊢ L w
case h.a.mp
α : Type u_1
L : Language α
w u v : Word α
h1 : u = ε
h2 : v ∈ L
h3 : w = u * v
⊢ L w