case some σ =>
  simp [stringAlgebra, RankedAlphabet.lift] at w
  generalize hw : w ⟨0, stringAlgebra.proof_1⟩ = w'
  simp [treeₑ, Function.comp]
  funext ⟨i, hi⟩
  have hi : i = 0 := by 
    simp [RankedAlphabet.lift] at hi
    cases i
    case zero => rfl
    case succ => contradiction
  simp [hw, hi]
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ treeₑ (σ⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some σ) (treeₑ ∘ w)
no goals