Definition build_term' {V: varspec σ} (nm: names σ) : iterfun (vec_map (term σ V) (arity (namelift V nm))) (term σ V (sort (namelift V nm))) := build_gterm' (namelift V nm).
Require Import UniMath.Foundations.All. Require Import UniMath.Algebra.Universal.SortedTypes.