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 Γ
σ : Γ
w : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ)) → Term (RankedAlphabet.lift Γ) Empty
hi : ∀ (a : Fin (RankedAlphabet.rank (RankedAlphabet.lift Γ) (some σ))), ∃ a_1, treeₑ a_1 = w a
⊢ ∃ a, treeₑ a = app (some σ) w
no goals