simp [Function.Injective]
Γ : Type
inst✝ : Alphabet Γ
⊢ Function.Injective
    { hom := treeₑ,
        property :=
          (_ :
            ∀ (σ : (RankedAlphabet.lift Γ).alphabet)
              (w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) σ),
              treeₑ (Algebra.θ (stringAlgebra Γ) σ w) =
                Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) σ (treeₑ ∘ w)) }.hom
Γ : Type
inst✝ : Alphabet Γ
⊢ ∀ (a₁ a₂ : (stringAlgebra Γ).carrier), treeₑ a₁ = treeₑ a₂ → a₁ = a₂