constructor
case h.a
α : Type u_1
L : Language α
w : Word α
⊢ (L ∘ₗ epsilon) w ↔ L w
case h.a.mp
α : Type u_1
L : Language α
w : Word α
⊢ (L ∘ₗ epsilon) w → L w

case h.a.mpr
α : Type u_1
L : Language α
w : Word α
⊢ L w → (L ∘ₗ epsilon) w