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