. intro n
  match n with
  | ⟨_,_,h,_,_⟩ =>
    apply False.elim h
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
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ ∅ → w ∈ ∅ ∘ₗ L