induction σ₁ generalizing σ₂ <;> cases σ₂ <;> simp [treeₑ, Term.algebra] at *
Γ : Type
inst✝ : Alphabet Γ
σ₁ σ₂ : (stringAlgebra Γ).carrier
h : treeₑ σ₁ = treeₑ σ₂
⊢ σ₁ = σ₂
case cons.cons
Γ : Type
inst✝ : Alphabet Γ
head✝¹ : Γ
tail✝¹ : List Γ
tail_ih✝ : ∀ (σ₂ : (stringAlgebra Γ).carrier), treeₑ tail✝¹ = treeₑ σ₂ → tail✝¹ = σ₂
head✝ : Γ
tail✝ : List Γ
h : some head✝¹ = some head✝ ∧ (fun x => treeₑ tail✝¹) = fun x => treeₑ tail✝
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝