cases σ
Γ : Type
inst✝ : Alphabet Γ
σ : (RankedAlphabet.lift Γ).alphabet
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) σ
⊢ treeₑ (Algebra.θ (stringAlgebra Γ) σ w) = Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) σ (treeₑ ∘ w)
case none
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ treeₑ (Algebra.θ (stringAlgebra Γ) none w) = Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) none (treeₑ ∘ w)

case some
Γ : Type
inst✝ : Alphabet Γ
val✝ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some val✝)
⊢ treeₑ (Algebra.θ (stringAlgebra Γ) (some val✝) w) =
    Algebra.θ (Term.algebra (RankedAlphabet.lift Γ) Empty) (some val✝) (treeₑ ∘ w)