simp [Term.algebra, Algebra.ops, Membership.mem]
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
v : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), v a ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
⊢ { fst := RankedAlphabet.rank Δ σ, snd := app σ } ∈ Algebra.ops (Term.algebra Δ H)
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
v : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), v a ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
⊢ ∃ σ_1 h, app σ_1 = (_ : RankedAlphabet.rank Δ σ = RankedAlphabet.rank Δ σ_1) ▸ app σ