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