case none =>
  simp [Function.comp, treeₑ, Term.algebra]
  funext ⟨_, h⟩
  simp [RankedAlphabet.lift] at h
  contradiction
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ treeₑ Word.ε = app none (treeₑ ∘ w)
no goals