constructor
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ ∘ₗ L ↔ w ∈ ∅
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ ∘ₗ L → w ∈ ∅

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ ∅ ∘ₗ L