case app σ v hi =>
  refine Closure.app ?_ hi
  simp [Term.algebra, Algebra.ops, Membership.mem]
  exists σ, rfl
Δ : 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))
⊢ app σ v ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
no goals