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