Definition build_gterm' {σ: signature} (nm: names σ) : iterfun (vec_map (term σ) (arity nm)) (term σ (sort nm)) := currify (build_term nm).
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.Universal.SortedTypes.