simp [Function.comp, treeₑ, Term.algebra]
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ treeₑ Word.ε = app none (treeₑ ∘ w)
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ (fun x => nomatch x) = fun x => treeₑ (w x)