simp [stringAlgebra, RankedAlphabet.lift] at w
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)
⊢ treeₑ (σ⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some σ) (treeₑ ∘ w)
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
w : (Γ⋆)⋆1
⊢ treeₑ (σ⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some σ) (treeₑ ∘ w)