case cons.cons σ _ hi _ _ =>
  have ⟨h₁, h₂⟩ := h
  injection h₁ with h₁          
  have : Nonempty (Fin $ (RankedAlphabet.lift Γ).rank $ some σ) := 
    .intro ⟨0, by simp [RankedAlphabet.lift]⟩ 
  simp [h₁, hi _ (const_func_ext h₂)]
Γ : Type
inst✝ : Alphabet Γ
σ : Γ
tail✝¹ : List Γ
hi : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some σ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
⊢ σ :: tail✝¹ = head✝ :: tail✝
no goals