constructor
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ (w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) ↔
    w ∈ Set.singleton Word.ε
case mp
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ (w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) →
    w ∈ Set.singleton Word.ε

case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ w ∈ Set.singleton Word.ε →
    w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })