simp [RankedAlphabet.lift] at hi
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
i : Nat
hi : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ i = 0
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi✝ : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
a : (stringAlgebra Γ).carrier
h : treeₑ a = w { val := 0, isLt := (_ : 0 < 1) }
i : Nat
hi : i < 1
⊢ i = 0