Definition nat2term (n: nat): gterm nat_signature nat_sort := nat_rect (λ _, gterm nat_signature nat_sort) nat_zero (λ (n: nat) (tn: gterm nat_signature nat_sort), nat_succ tn) n.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.MoreLists. Require Import UniMath.Algebra.Universal.Algebras. Require Import UniMath.Algebra.Universal.Terms.