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