simp [h']
Δ : 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
no goals