case none => 
  exists .ε
  simp [treeₑ, Term.algebra]
  funext ⟨_, h⟩
  simp [RankedAlphabet.lift] at h
  contradiction
Γ : Type
inst✝ : Alphabet Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) none)), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app none w
no goals