case app σ w hi =>
  cases σ 
  case none => 
    exists .ε
    simp [treeₑ, Term.algebra]
    funext ⟨_, h⟩
    simp [RankedAlphabet.lift] at h
    contradiction
  case some σ => 
    have ⟨a, h⟩ := hi ⟨0, by simp [RankedAlphabet.lift]⟩
    exists σ⬝a
    simp [h, treeₑ]
    refine congrArg _ ?_
    funext ⟨i, hi⟩
    have hi : i = 0 := by 
      simp [RankedAlphabet.lift] at hi
      cases i
      case zero => rfl
      case succ => contradiction
    simp [hi]
Γ : Type
inst✝ : Alphabet Γ
σ : (RankedAlphabet.lift Γ).alphabet
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) σ) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) σ)), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app σ w
no goals