exact {
  hom := treeₑ
  property := by
    intro σ w
    cases σ
    all_goals simp [Term.algebra, stringAlgebra]
    case none =>
      simp [Function.comp, treeₑ, Term.algebra]
      funext ⟨_, h⟩
      simp [RankedAlphabet.lift] at h
      contradiction
    case some σ =>
      simp [stringAlgebra, RankedAlphabet.lift] at w
      generalize hw : w ⟨0, stringAlgebra.proof_1⟩ = w'
      simp [treeₑ, Function.comp]
      funext ⟨i, hi⟩
      have hi : i = 0 := by 
        simp [RankedAlphabet.lift] at hi
        cases i
        case zero => rfl
        case succ => contradiction
      simp [hw, hi]
  bij := {
    inj := by 
      simp [Function.Injective]
      intro σ₁ σ₂ h
      induction σ₁ generalizing σ₂ <;> cases σ₂ <;> simp [treeₑ, Term.algebra] at *
      case cons.cons σ _ hi _ _ =>
        have ⟨h₁, h₂⟩ := h
        injection h₁ with h₁          
        have : Nonempty (Fin $ (RankedAlphabet.lift Γ).rank $ some σ) := 
          .intro ⟨0, by simp [RankedAlphabet.lift]⟩ 
        simp [h₁, hi _ (const_func_ext h₂)]
    surj := by
      simp [Function.Surjective]
      intro a
      induction a
      case var => contradiction
      case app σ w hi =>
        cases σ 
        case none => 
          exists .ε
          simp [treeₑ, Term.algebra]
          funext ⟨_, h⟩
          simp [RankedAlphabet.lift] at h
          contradiction
        case some σ => 
          have ⟨a, h⟩ := hi ⟨0, by simp [RankedAlphabet.lift]⟩
          exists σ⬝a
          simp [h, treeₑ]
          refine congrArg _ ?_
          funext ⟨i, hi⟩
          have hi : i = 0 := by 
            simp [RankedAlphabet.lift] at hi
            cases i
            case zero => rfl
            case succ => contradiction
          simp [hi]
  }
}
case val
Γ : Type
inst✝ : Alphabet Γ
⊢ Iso (stringAlgebra Γ) (Term.algebra (RankedAlphabet.lift Γ) Empty)
no goals