simp [RankedAlphabet.lift] at hi
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ i = 0
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi : i < 1
⊢ i = 0