have hi : i = 0 := by 
  simp [RankedAlphabet.lift] at hi
  cases i
  case zero => rfl
  case succ => contradiction
case h
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ treeₑ w' = treeₑ (w { val := i, isLt := hi })
case h
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
w' : Γ⋆
hw : w { val := 0, isLt := stringAlgebra.proof_1 } = w'
i : Nat
hi✝ : i < RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
hi : i = 0
⊢ treeₑ w' = treeₑ (w { val := i, isLt := hi✝ })