all_goals simp [Term.algebra, stringAlgebra]
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)
case none
Γ : Type
inst✝ : Alphabet Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) none
⊢ treeₑ Word.ε = app none (treeₑ ∘ w)

case some
Γ : Type
inst✝ : Alphabet Γ
val✝ : Γ
w : (stringAlgebra Γ).carrier⋆RankedAlphabet.rank (RankedAlphabet.lift Γ) (some val✝)
⊢ treeₑ (val✝⬝w { val := 0, isLt := stringAlgebra.proof_1 }) = app (some val✝) (treeₑ ∘ w)