simp [Set.singleton, Membership.mem] at *
case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' : 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 })
case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' : w = Word.ε
⊢ match w with
  | [] => True
  | i :: tl => ∃ h_1, Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 }) tl