simp [Function.Surjective]
Γ : Type
inst✝ : Alphabet Γ
⊢ Function.Surjective
    { 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 Γ
⊢ ∀ (b : (Term.algebra (RankedAlphabet.lift Γ) Empty).carrier), ∃ a, treeₑ a = b