fact: 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).
imports: UniMath.Foundations.All UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Terms